Commit 2022-11-18 03:37 bffd1500

View on Github →

feat: port Order.RelClasses (#560) mathlib3 hash: fd47bdf09e90f553519c712378e651975fe8c829

depends on: #556

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/RelClasses.lean

added theorem IsAntisymm.swap

added theorem IsAsymm.swap

added theorem IsIrrefl.swap

added theorem IsLinearOrder.swap

added theorem IsOrderConnected.neg_trans

added theorem IsPartialOrder.swap

added theorem IsPreorder.swap

added theorem IsRefl.swap

added theorem IsStrictOrder.swap

added theorem IsStrictTotalOrder.swap

added theorem IsTotal.swap

added theorem IsTotalPreorder.swap

added theorem IsTrans.swap

added theorem IsTrichotomous.swap

added theorem IsWellFounded.apply

added def IsWellFounded.fix

added theorem IsWellFounded.fix_eq

added theorem IsWellFounded.induction

added def IsWellFounded.toWellFoundedRelation

added theorem IsWellFounded_iff

added def IsWellOrder.toHasWellFounded

added def Set.Bounded

added def Set.Unbounded

added theorem Set.not_bounded_iff

added theorem Set.not_unbounded_iff

added theorem Set.unbounded_of_isEmpty

added theorem Subrelation.isWellFounded

added theorem Subsingleton.isWellOrder

added theorem WellFounded.asymmetric

added theorem WellFoundedGt.apply

added def WellFoundedGt.fix

added theorem WellFoundedGt.fix_eq

added theorem WellFoundedGt.induction

added def WellFoundedGt.toWellFoundedRelation

added def WellFoundedGt

added theorem WellFoundedLt.apply

added def WellFoundedLt.fix

added theorem WellFoundedLt.fix_eq

added theorem WellFoundedLt.induction

added def WellFoundedLt.toWellFoundedRelation

added def WellFoundedLt

added theorem WellFoundedRelation.asymmetric

added theorem antisymm'

added theorem antisymm_iff

added theorem antisymm_of'

added theorem antisymm_of

added theorem comm

added theorem comm_of

added theorem empty_relation_apply

added theorem eq_empty_relation

added theorem eq_or_ssubset_of_subset

added theorem extensional_of_trichotomous_of_irrefl

added theorem isStrictWeakOrder_of_isOrderConnected

added def linearOrderOfSTO

added theorem ne_of_irrefl'

added theorem ne_of_irrefl

added theorem ne_of_not_subset

added theorem ne_of_not_superset

added theorem ne_of_ssubset

added theorem ne_of_ssuperset

added theorem not_rel_of_subsingleton

added theorem not_ssubset_of_subset

added theorem not_subset_of_ssubset

added theorem of_eq

added def partialOrderOfSO

added theorem rel_of_subsingleton

added theorem right_iff_left_not_left

added theorem right_iff_left_not_left_of

added theorem ssubset_asymm

added theorem ssubset_iff_subset_ne

added theorem ssubset_iff_subset_not_subset

added theorem ssubset_irrefl

added theorem ssubset_irrfl

added theorem ssubset_of_ne_of_subset

added theorem ssubset_of_ssubset_of_subset

added theorem ssubset_of_subset_not_subset

added theorem ssubset_of_subset_of_ne

added theorem ssubset_of_subset_of_ssubset

added theorem ssubset_or_eq_of_subset

added theorem ssubset_trans

added theorem subset_antisymm

added theorem subset_antisymm_iff

added theorem subset_iff_ssubset_or_eq

added theorem subset_of_eq

added theorem subset_of_ssubset

added theorem subset_refl

added theorem subset_rfl

added theorem subset_trans

added theorem superset_antisymm

added theorem superset_antisymm_iff

added theorem superset_of_eq

added theorem trans_trichotomous_left

added theorem trans_trichotomous_right

added theorem transitive_ge

added theorem transitive_gt

added theorem transitive_le

added theorem transitive_lt

added theorem transitive_of_trans

added theorem wellFoundedGt_dual_iff

added theorem wellFoundedLt_dual_iff