Leibniz' Project

A website aiming at global formalization

Table of contents

Rocq index

ActionProfile (definition)

add1_lt (lemma)

admits_omnipotent (definition)

aggregation_preferences (definition)

agree_on (definition)

agree_on_implies_remove_indifference_equal (lemma)

agree_on_implies_remove_indifference_equal_profile (lemma)

agree_on_profile (definition)

altruist (definition)

always_follows_its_ethic (definition)

antecedent (definition)

antecedent_exists (lemma)

antecedent_not_exists (lemma)

Arrow (theorem)

assertion_1 (lemma)

assertion_2 (lemma)

assertion_3 (lemma)

assertion_4 (lemma)

associated_utility (definition)

associatedPreferenceSpace (definition)

assymmetric (definition)

bipartite_contest (definition)

bottom_choice (definition)

can_achieve (definition)

can_achieve_all (definition)

can_achieve_ethically (definition)

can_achieve_with_ethics (definition)

can_all_achieve_ethically (definition)

can_be_obtained (definition)

can_win_conflict (definition)

can_win_conflict_with_ethics (definition)

cannot_win_conflict (definition)

cannot_win_conflict_with_ethics (definition)

compatible (definition)

composition (definition)

conflict (definition)

Constitution (definition)

corollary_2 (corollary)

corollary_3 (corollary)

countable (definition)

dead_end (definition)

deterministic_iff_no_indeterminism (lemma)

deterministic_many_worlds_interpretation (lemma)

deterministic_World (definition)

dictator (definition)

dictator_except (definition)

dominant (definition)

dominant_strategies_profile (definition)

dominant_strategies_well_named (lemma)

dominant_strategy (definition)

eq_symmetric (lemma)

equipotent (definition)

Ethic (definition)

ethic_restricts_conflict_winning (lemma)

ethic_restricts_goal_achieving (lemma)

ethic_restricts_goal_achieving_with_ethics (lemma)

ethic_strictly_restricts_goal_achieving (lemma)

ethic_subjective_to_dynamic (definition)

EthicalProfile (definition)

ethicless (definition)

ethicless_least_restrictive (lemma)

ethics_cant_help_goal_achieving (lemma)

Event (definition)

every_ethic_more_restrictive_than_itself (lemma)

every_ethic_without_dead_end_is_utilitarian (proposition)

everyone_always_follows_its_ethic_dynamic (definition)

everyone_always_same_ethic (definition)

everyone_follows_its_ethic (definition)

everyone_follows_its_ethic_dynamic (definition)

everyone_is_objective (definition)

everyone_same_ethic (definition)

exists_dominant_strategy (lemma)

exists_of_not_extremal (lemma)

exists_pivot (lemma)

exists_pivot_when_hater (lemma)

extends (definition)

extremal_lemma (lemma)

false_to_False (lemma)

follows_its_ethic (definition)

GameForm (definition)

generalized_whole_society (definition)

get_action (definition)

get_carrier (definition)

get_h1 (definition)

get_h2 (definition)

get_injection (definition)

get_preference_order (definition)

get_state (definition)

get_SubjectiveState (definition)

get_t1 (definition)

get_t2 (definition)

get_time (definition)

Gibbard (theorem)

GibbardSatterthwaite (corollary)

GoalProfile (definition)

happens_in (definition)

has_pivot (definition)

History (definition)

HistoryBefore (definition)

HistoryUntil (definition)

identity (definition)

identity_permutation (definition)

ignore_actions (definition)

in_image (definition)

incompatible (definition)

independence_irrelevant_alternatives (definition)

Indeterminism (definition)

indeterministic_iff_any_indeterminism (lemma)

indifferent (definition)

indifferent_if_non_strict_both_ways (lemma)

indifferent_reflexive (lemma)

indifferent_symmetric (lemma)

indifferent_transitive (lemma)

IndividualEthic (definition)

IndividualRank (definition)

IndividualsPermutationOnStates (definition)

inj_implies_antecedent_unique (lemma)

instance_indeterminism (definition)

irreflexive (definition)

is_deterministic (definition)

is_deterministic_except_for_free_will (definition)

is_maximum (definition)

is_pivotal (definition)

is_possible (definition)

is_utilitarian (definition)

le_mathcomp_equivalent (lemma)

le_preference_order (lemma)

le_PreferenceOrder (definition)

le_total (lemma)

le_transitive (lemma)

leaves_no_freedom (definition)

lt_mathcomp_equivalent (lemma)

lt_mathcomp_equivalent_not (lemma)

make_above (definition)

make_above_preference (definition)

make_above_preference_order (lemma)

make_above_profile (definition)

make_above_total (lemma)

make_above_transitive (lemma)

make_above_well_named (lemma)

make_very_bottom (definition)

make_very_bottom_preference (definition)

make_very_bottom_preference_order (lemma)

make_very_bottom_total (lemma)

make_very_bottom_transitive (lemma)

make_very_top (definition)

make_very_top_at (definition)

make_very_top_preference (definition)

make_very_top_preference_order (lemma)

make_very_top_total (lemma)

make_very_top_transitive (lemma)

make_very_top_well_named (lemma)

manipulable (definition)

many_worlds_extension (definition)

map_PreferenceOrder (definition)

map_relation (definition)

maximizes (definition)

may_disapprove (definition)

may_never_disapprove (definition)

more_restrictive (definition)

more_restrictive_dynamic (definition)

more_restrictive_ethic_diminishes_conflicts (proposition)

more_restrictive_ethic_strictly_diminishes_conflicts (proposition)

never_leaves_freedom (definition)

never_leaves_freedom_implies_never_has_dead_end (corollary)

no_conflict (definition)

no_dead_end_if_altruist (lemma)

no_dead_end_if_conflict (definition)

no_dead_end_if_everyone_follows_its_ethic (lemma)

no_dead_end_if_no_conflict (definition)

no_ethic_strictly_more_restrictive_than_itself (lemma)

no_freedom_implies_no_dead_end (lemma)

nobody_may_disapprove (definition)

nobody_may_ever_disapprove (definition)

non_strict (definition)

non_strict_stable_by_indifferent (lemma)

non_strict_stable_by_indifferent' (lemma)

non_strict_strict_transitive (lemma)

non_strict_transitive (lemma)

not_bigger_than (definition)

not_bigger_than_transitive (definition)

not_extremal (lemma)

not_very_top_or_not_very_bottom (lemma)

objective (definition)

objective_ethics_may_never_disapprove_implies_same_ethic (proposition)

objective_ethics_no_disapproval_iff_same_ethic (corollary)

omnipotent (definition)

outcome_when_dominant_strategies (definition)

pairwise_determination (lemma)

permutation_subjective_state (definition)

PermutationOnIndividuals (definition)

PhysicalTheory (definition)

pivot_implies_dictator (lemma)

pivot_implies_dictator_except (lemma)

preference_antisym_iff_total_order (lemma)

preference_order (definition)

preference_order_reflexive (lemma)

preference_order_stable_by_flip (lemma)

preference_order_stable_by_map (lemma)

PreferenceOrder (definition)

PreferenceProfile (definition)

PreferenceSpace (structure)

preferred_when_dominant_strategies (definition)

preferred_when_dominant_strategies_strict_implies_nonstrict (lemma)

profile_III (definition)

proj_individual_SubjectiveState (lemma)

proj_state_SubjectiveState (lemma)

remove_indifference (definition)

remove_indifference_down_to_littlest_subset (lemma)

remove_indifference_in_Z_out_Z (lemma)

remove_indifference_is_preference_order (corollary)

remove_indifference_is_total_order (lemma)

remove_indifference_PreferenceOrder (definition)

remove_indifference_PreferenceProfile (definition)

remove_indifference_profile (definition)

remove_indifference_profile_down_to_littlest_subset (lemma)

remove_indifference_strict_unchanged_on_Z (lemma)

remove_indifference_well_named (lemma)

respects_unanimity (definition)

reverse (definition)

reverse_very_bottom (lemma)

same_ethic_implies_may_not_disapprove (lemma)

same_order (definition)

same_order_characterization (lemma)

same_order_non_strict (lemma)

same_order_reflexive (lemma)

same_order_strict_case (lemma)

same_order_symmetric (lemma)

satisfies (definition)

second_equal_or_1st_unequal (definition)

second_equal_or_1st_unequal_preference_order (lemma)

single_bottom_others_indifferent (definition)

single_bottom_very_bottom (lemma)

single_min_all_others_indifferent_preference_profile (definition)

single_top_others_indifferent (definition)

single_top_very_top (lemma)

smaller_than (definition)

smaller_than_assymmetric (lemma)

smaller_than_irreflexive (lemma)

smaller_than_transitive (definition)

State_dynamic (definition)

state_dynamic (definition)

state_dynamic_to_subjective (definition)

straightforward (definition)

Strategy_VotingScheme (definition)

StrategyProfile (definition)

StrategyProfile_VotingScheme (definition)

strict (definition)

strict_asymmetric (lemma)

strict_implies_non_strict (lemma)

strict_implies_unequal (lemma)

strict_irreflexive (lemma)

strict_le_is_lt (lemma)

strict_non_strict_transitive (lemma)

strict_preference (definition)

strict_transitive (lemma)

strictly_more_restrictive (definition)

strictly_more_restrictive_dynamic (definition)

strictly_preferred_when_dominant_strategies (definition)

strictly_preferred_when_dominant_strategies_respects_unanimity (corollary)

SubjectiveState (structure)

switch_strict_preference_is_preference (lemma)

switch_strictness (definition)

switch_strictness_involutive (lemma)

switch_strictness_preferred_when_dominant_strategies (lemma)

switch_strictness_preferred_when_dominant_strategies' (lemma)

third_alt (definition)

top_choice (definition)

total (definition)

total_is_reflexive (lemma)

total_order (definition)

total_order_is_antisymmetric_preference (lemma)

total_stable_by_flip (lemma)

TotalOrder (definition)

transitivity_stable_by_flip (lemma)

unanimous_altruism_not_enough_to_avoid_conflicts (proposition)

unanimous_very_bottom (lemma)

unanimous_very_bottom_choice (definition)

unanimous_very_extremal_choice (definition)

unanimous_very_top (lemma)

unanimous_very_top_choice (definition)

unanimously_prefers (definition)

unanimously_same_order (definition)

unanimously_same_order_symmetric (lemma)

utilitarian_ethic_always_unique_maximum (definition)

utilitarian_ethic_never_freedom_iff_always_maximum_for_unique_action (corollary)

utilitarian_ethic_no_freedom_iff_maximum_for_unique_action (proposition)

utilitarian_ethic_unique_maximum (definition)

UtilityFunction (definition)

very_bottom_choice (definition)

very_extremal_choice (definition)

very_top_choice (definition)

VotingScheme (definition)

with_constraints (definition)

without_dead_end (definition)