Unbundled

📁 Source: Mathlib/Order/Defs/Unbundled.lean

Statistics

Metric	Count
Definitions AntiSymmetric, EmptyRelation, Irreflexive, IsAntisymm, IsAsymm, IsEquiv, IsIrrefl, IsLinearOrder, IsLowerSet, IsPartialOrder, IsPreorder, IsRefl, IsRelLowerSet, IsRelUpperSet, IsStrictOrder, IsStrictTotalOrder, IsStrictWeakOrder, IsSymm, IsTotal, IsTrans, IsTrichotomous, IsUpperSet, LowerSet, carrier, MaximalFor, MinimalFor, RelLowerSet, carrier, RelUpperSet, carrier, Total, UpperSet, carrier, instTransOfIsTrans	34
Theorems isTrans, reflexive, symmetric, transitive, irrefl, irreflexive, isTrans, trans, isAntisymm, isIrrefl, toIsPreorder, toSymm, toIsPartialOrder, toTotal, toAntisymm, toIsPreorder, toIsTrans, toRefl, toIrrefl, toIsTrans, toIsStrictOrder, toTrichotomous, incomp_trans, toIsStrictOrder, decide, trans, lower', le_of_ge, prop, le_of_le, prop, le_of_le, prop, le_of_le, prop, isRelLowerSet', isRelUpperSet', decide, antisymm, decide, irrefl, isAntisymm, isIrrefl, decide, decide, decide, decide, isTrichotomous, to_refl, trichotomous, decide, upper', antisymm, antisymm', antisymm_iff, antisymm_of, antisymm_of', asymm, asymm_of, asymm_of_isTrans_of_irrefl, comm, comm_of, empty_relation_apply, eq_isEquiv, extensional_of_trichotomous_of_irrefl, iff_isEquiv, instIrreflEmptyRelation_mathlib, instIsTransOfTrans, irrefl, irrefl_of, isTrans_def, ne_of_irrefl, ne_of_irrefl', not_rel_of_subsingleton, of_eq, refl, refl_of, rel_congr, rel_congr_left, rel_congr_right, rel_of_subsingleton, symm_of, total_of, trans, trans_of, trans_trichotomous_left, trans_trichotomous_right, transitive_of_trans, trichotomous, trichotomous_of	90
Total	124

Equivalence

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isTrans 📖	mathematical	—	IsTrans	—	—
reflexive 📖	mathematical	—	Reflexive	—	—
symmetric 📖	mathematical	—	Symmetric	—	—
transitive 📖	mathematical	—	IsTrans	—	isTrans

InvImage

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
irrefl 📖	—	—	—	—	—
irreflexive 📖	—	—	—	—	irrefl
isTrans 📖	mathematical	—	IsTrans	—	IsTrans.trans
trans 📖	mathematical	—	IsTrans	—	isTrans

IsAsymm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isAntisymm 📖	—	—	—	—	Std.Asymm.antisymm
isIrrefl 📖	—	—	—	—	Std.Asymm.irrefl

IsEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toIsPreorder 📖	mathematical	—	IsPreorder	—	—
toSymm 📖	—	—	—	—	—

IsLinearOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toIsPartialOrder 📖	mathematical	—	IsPartialOrder	—	—
toTotal 📖	—	—	—	—	—

IsPartialOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toAntisymm 📖	—	—	—	—	—
toIsPreorder 📖	mathematical	—	IsPreorder	—	—

IsPreorder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toIsTrans 📖	mathematical	—	IsTrans	—	—
toRefl 📖	—	—	—	—	—

IsStrictOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toIrrefl 📖	—	—	—	—	—
toIsTrans 📖	mathematical	—	IsTrans	—	—

IsStrictTotalOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toIsStrictOrder 📖	mathematical	—	IsStrictOrder	—	—
toTrichotomous 📖	—	—	—	—	—

IsStrictWeakOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
incomp_trans 📖	—	—	—	—	—
toIsStrictOrder 📖	mathematical	—	IsStrictOrder	—	—

IsTrans

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
decide 📖	mathematical	—	IsTrans	—	trans
trans 📖	—	—	—	—	—

LowerSet

Definitions

Name	Category	Theorems
carrier 📖	CompOp	6 math math: Order.Ideal.directed', Order.Ideal.nonempty', Order.Ideal.carrier_eq_coe, IsClosed.lowerClosure, lower', carrier_eq_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lower' 📖	mathematical	—	IsLowerSet carrier	—	—

Maximal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_of_ge 📖	—	Maximal	—	—	—
prop 📖	—	Maximal	—	—	—

MaximalFor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_of_le 📖	—	MaximalFor	—	—	—
prop 📖	—	MaximalFor	—	—	—

Minimal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_of_le 📖	—	Minimal	—	—	—
prop 📖	—	Minimal	—	—	—

MinimalFor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_of_le 📖	—	MinimalFor	—	—	—
prop 📖	—	MinimalFor	—	—	—

RelLowerSet

Definitions

Name	Category	Theorems
carrier 📖	CompOp	1 math math: isRelLowerSet'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isRelLowerSet' 📖	mathematical	—	IsRelLowerSet carrier	—	—

RelUpperSet

Definitions

Name	Category	Theorems
carrier 📖	CompOp	1 math math: isRelUpperSet'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isRelUpperSet' 📖	mathematical	—	IsRelUpperSet carrier	—	—

Std.Antisymm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
decide 📖	—	—	—	—	—

Std.Asymm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antisymm 📖	—	—	—	—	—
decide 📖	—	—	—	—	—
irrefl 📖	—	—	—	—	—
isAntisymm 📖	—	—	—	—	antisymm
isIrrefl 📖	—	—	—	—	irrefl

Std.Irrefl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
decide 📖	—	—	—	—	—

Std.Refl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
decide 📖	—	—	—	—	—

Std.Symm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
decide 📖	—	—	—	—	—

Std.Total

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
decide 📖	—	—	—	—	—
isTrichotomous 📖	—	—	—	—	trichotomous
to_refl 📖	—	—	—	—	—
trichotomous 📖	—	—	—	—	—

Std.Trichotomous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
decide 📖	—	—	—	—	—

UpperSet

Definitions

Name	Category	Theorems
carrier 📖	CompOp	2 math math: upper', carrier_eq_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
upper' 📖	mathematical	—	IsUpperSet carrier	—	—

(root)

Definitions

Name	Category	Theorems
AntiSymmetric 📖	MathDef	—
EmptyRelation 📖	MathDef	—
Irreflexive 📖	MathDef	—
IsAntisymm 📖	MathDef	—
IsAsymm 📖	MathDef	—
IsEquiv 📖	CompData	8 math math: IsConjRoot.instIsEquiv, LocalizedModule.r.isEquiv, eq_isEquiv, Order.Preimage.instIsEquiv, Quotient.instIsEquivEquiv, Ne.instIsEquiv_compl, iff_isEquiv, Path.Homotopic.instIsEquiv
IsIrrefl 📖	MathDef	—
IsLinearOrder 📖	CompData	4 math math: extend_partialOrder, RelEmbedding.isLinearOrder, instIsLinearOrderGe, instIsLinearOrderLe
IsLowerSet 📖	MathDef	85 math math: Order.IsIdeal.IsLowerSet, IsUpperSet.ofDual, IsLowerSet.smul, IsLowerSet.sdiff_of_isUpperSet, IsLowerSet.prod, isRelLowerSet_true_iff_isLowerSet, PrincipalSeg.isLowerSet_range, Topology.IsLowerSet.isOpen_iff_isLowerSet, Concept.isLowerSet_extent_lt, IsUpperSet.compl, IsLowerSet.add_right, Order.Ideal.lower, isUpperSet_preimage_toDual_iff, IsLowerSet.memberSubfamily, isLowerSet_iff_Iic_subset, Topology.IsScott.isClosed_iff_isLowerSet_and_dirSupClosed, isLowerSet_univ, Relation.fibration_iff_isLowerSet_image, IsLowerSet.vadd, isLowerSet_iUnion₂, IsLowerSet.preimage, isLowerSet_preimage_toDual_iff, HasUpperLowerClosure.isLowerSet_closure, LinearMap.isLowerSet_support_singularValues, Topology.IsUpper.isLowerSet_of_isClosed, IsLowerSet.closure, isLowerSet_iInter₂, isLowerSet_iUnion, IsLowerSet.cthickening, isLowerSet_Iio, Topology.WithLowerSet.isLowerSet_toLowerSet_preimage, IsUpperSet.neg, Finsupp.isLowerSet_range_embDomain, Relation.Fibration.isLowerSet_image, isLowerSet_sInter, IsLowerSet.sub_right, YoungDiagram.isLowerSet, isLowerSet_preimage_ofDual_iff, IsUpperSet.sub_left, IsLowerSet.nonMemberSubfamily, Topology.IsUpperSet.isClosed_iff_isLower, Concept.isLowerSet_extent_le, isLowerSet_setOf, IsUpperSet.inv, isLowerSet_subtype_iff_isRelLowerSet, isLowerSet_compl, isUpperSet_preimage_ofDual_iff, Set.antitone_mem, IsUpperSet.div_left, isUpperSet_compl, Finset.isLowerSet_shatterer, IsLowerSet.union, isLowerSet_sUnion, Order.isIdeal_iff, Topology.WithLowerSet.isOpen_ofLowerSet_preimage, Finset.shatterer_eq, IsLowerSet.thickening, Topology.IsScott.isLowerSet_of_isClosed, isLowerSet_iff_forall_lt, Topology.IsLower.isLowerSet_of_isOpen, IsLowerSet.erase, isLowerSet_iff_Iio_subset, IsLowerSet.image_fibration, isLowerSet_empty, IsUpperSet.toDual, isLowerSet_iInter, IsLowerSet.mul_left, exists_isClopen_upper_or_lower_of_ne, Relation.fibration_iff_isLowerSet_image_Iic, IsUpperSet.isLowerSet_preimage_coe, LowerSet.lower', IsLowerSet.thickening', IsLowerSet.div_right, exists_isClopen_lower_of_not_le, LowerSet.lower, IsLowerSet.sdiff, IsLowerSet.mul_right, lowerClosure_eq, IsLowerSet.cthickening', InitialSeg.isLowerSet_range, IsLowerSet.add_left, IsLowerSet.inter, IsLowerSet.interior, IsLowerSet.image, isLowerSet_Iic
IsPartialOrder 📖	CompData	12 math math: IsLinearOrder.toIsPartialOrder, List.instIsPartialOrderIsPrefix, RelEmbedding.isPartialOrder, List.instIsPartialOrderIsInfix, instIsPartialOrderSetIsExtreme, Graph.IsInducedSubgraph.instIsPartialOrder, List.instIsPartialOrderIsSuffix, Graph.IsClosedSubgraph.instIsPartialOrder, Graph.IsSpanningSubgraph.instIsPartialOrder, IsPartialOrder.swap, instIsPartialOrderLe, instIsPartialOrderGe
IsPreorder 📖	CompData	11 math math: IsPreorder.swap, SimpleGraph.instIsPreorderIsContained, instIsPreorderPFunNatTuringReducible, instIsPreorderLe, SimpleGraph.instIsPreorderIsIndContained, IsEquiv.toIsPreorder, Order.Preimage.instIsPreorder, IsPartialOrder.toIsPreorder, Subrel.instIsPreorderSubtype, instIsPreorderGe, RelEmbedding.isPreorder
IsRefl 📖	MathDef	—
IsRelLowerSet 📖	MathDef	18 math math: isRelLowerSet_true_iff_isLowerSet, isRelLowerSet_Icc_ge, IsRelLowerSet.union, IsRelLowerSet.iUnion₂, IsRelLowerSet.inter, IsRelLowerSet.mono_isLowerSet, IsRelLowerSet.sInter, IsRelLowerSet.iInter₂, IsLowerSet.isRelLowerSet_sep, isRelLowerSet_empty, RelLowerSet.isRelLowerSet, isLowerSet_subtype_iff_isRelLowerSet, PreAbstractSimplicialComplex.isRelLowerSet_faces, IsRelLowerSet.sUnion, isRelLowerSet_self, RelLowerSet.isRelLowerSet', IsRelLowerSet.iInter, IsRelLowerSet.iUnion
IsRelUpperSet 📖	MathDef	17 math math: IsRelUpperSet.iInter, isRelUpperSet_true_iff_isUpperSet, isRelUpperSet_empty, IsRelUpperSet.union, IsRelUpperSet.sInter, IsUpperSet.isRelUpperSet_sep, IsRelUpperSet.iInter₂, RelUpperSet.isRelUpperSet', IsRelUpperSet.inter, isRelUpperSet_Icc_le, isUpperSet_subtype_iff_isRelUpperSet, IsRelUpperSet.iUnion, RelUpperSet.isRelUpperSet, IsRelUpperSet.mono_isUpperSet, IsRelUpperSet.iUnion₂, IsRelUpperSet.sUnion, isRelUpperSet_self
IsStrictOrder 📖	CompData	16 math math: Finsupp.Colex.isStrictOrder, RelEmbedding.isStrictOrder, Finsupp.Lex.isStrictOrder, Set.IsStrictOrder.subset, instIsStrictOrderGt, Order.Preimage.instIsStrictOrder, Pi.Colex.isStrictOrder, Subrel.instIsStrictOrderSubtype, DFinsupp.Lex.isStrictOrder, Finsupp.DegLex.isStrictOrder, IsStrictTotalOrder.toIsStrictOrder, IsStrictWeakOrder.toIsStrictOrder, IsStrictOrder.swap, Pi.Lex.isStrictOrder, DFinsupp.Colex.isStrictOrder, instIsStrictOrderLt
IsStrictTotalOrder 📖	CompData	6 math math: instIsStrictTotalOrderLt, IsStrictTotalOrder.swap, instIsStrictTotalOrderMonovaryOrder, instIsStrictTotalOrderOfIsWellOrder, instIsStrictTotalOrderGt, RelEmbedding.isStrictTotalOrder
IsStrictWeakOrder 📖	CompData	2 math math: Order.Preimage.instIsStrictWeakOrder, isStrictWeakOrder_of_isOrderConnected
IsSymm 📖	MathDef	—
IsTotal 📖	MathDef	—
IsTrans 📖	CompData	72 math math: instIsTransAntisymmRel, Associated.instIsTrans, Relation.isTrans_map, transitive_manyOneReducible, instIsTransDvd, instIsTransOfTrans, InvImage.isTrans, Finset.instIsTransSubset, Quotient.instIsTransLe, Relation.transitive_join, transitive_oneOneReducible, List.SublistForall₂.is_trans, InvImage.trans, Relation.isTrans_join, FirstOrder.Language.Theory.Iff.instIsTransBoundedFormula, IsStrictOrder.toIsTrans, transitive_gt, FirstOrder.Language.Relations.realize_transitive, Sigma.instIsTransLex, OrderDual.instIsTransLt, SemiconjBy.isTrans, isTrans_ge, Finset.instIsTransSSubset, transitive_le, Set.instIsTransSubset, instIsTransOfIsWellOrder, IsPreorder.toIsTrans, PSet.instIsTransSubset, IsTrans.decide, RelEmbedding.isTrans, ZFSet.IsOrdinal.isTrans, instIsTransGt, instIsTransLe, isTrans_manyOneReducible, FirstOrder.Language.Theory.Imp.instIsTransBoundedFormula, transitive_lt, Computation.LiftRel.trans, isTrans_lt, transitive_ge, ZFSet.isOrdinal_iff_isTrans, Relation.transitive_reflTransGen, instIsTransLt, IsTrans.comap, Sum.instIsTransLiftRel, IsTrans.swap, Equivalence.isTrans, Subrel.instIsTransSubtype, Prod.instIsTransLex, isTrans_gt, CategoryTheory.Abelian.pseudoEqual_trans, Relation.transitive_transGen, instIsTransGe, AddCommGroup.instIsTransModEq, OrderDual.instIsTransLe, Equivalence.transitive, ZFSet.instIsTransSubset, instIsTransNatLeHAddOfNat, isTrans_oneOneReducible, Set.instIsTransSSubset, AddSemiconjBy.transitive, isTrans_le, isTrans_def, Sum.instIsTransLex, Relation.instIsTransTransGen, AddSemiconjBy.isTrans, Transitive.comap, Int.ModEq.instIsTrans, Relation.map_transitive, Relation.instIsTransReflTransGen, SemiconjBy.transitive, Stream'.WSeq.LiftRel.trans, Order.Preimage.instIsTrans
IsTrichotomous 📖	MathDef	—
IsUpperSet 📖	MathDef	83 math math: UpperSet.upper', Topology.IsScott.isUpperSet_of_isOpen, IsLowerSet.div_left, isUpperSet_iff_forall_lt, upperClosure_eq, IsLowerSet.ofDual, Set.Intersecting.isUpperSet, IsUpperSet.vadd, Set.Intersecting.isUpperSet', isUpperSet_preimage_toDual_iff, IsUpperSet.add_right, Specialization.isOpen_toEquiv_preimage, isUpperSet_iUnion₂, isRelUpperSet_true_iff_isUpperSet, IsLowerSet.sub_left, IsUpperSet.interior, IsUpperSet.mul_right, isLowerSet_preimage_toDual_iff, Topology.IsUpperSet.isOpen_iff_isUpperSet, exists_isClopen_upper_of_not_le, IsUpperSet.sdiff, isUpperSet_Ioi, Topology.IsLowerSet.isClosed_iff_isUpper, IsUpperSet.preimage, IsUpperSet.thickening', IsUpperSet.div_right, Relation.fibration_iff_isUpperSet_image, IsLowerSet.compl, Topology.WithUpperSet.isUpperSet_toUpperSet_preimage, Topology.WithScott.isOpen_iff_isUpperSet_and_scottHausdorff_open', isUpperSet_iInter₂, isUpperSet_Ici, isLowerSet_preimage_ofDual_iff, ClopenUpperSet.upper, Set.monotone_mem, IsUpperSet.add_left, IsUpperSet.thickening, Concept.isUpperSet_intent_lt, IsUpperSet.mul_left, IsUpperSet.image_fibration, Concept.isUpperSet_intent_le, isLowerSet_compl, IsUpperSet.sdiff_of_isLowerSet, IsUpperSet.smul, isUpperSet_preimage_ofDual_iff, Topology.IsUpper.isUpperSet_of_isOpen, isUpperSet_compl, IsUpperSet.sub_right, IsLowerSet.isUpperSet_preimage_coe, IsUpperSet.inter, isUpperSet_setOf, Specialization.isUpperSet_ofEquiv_preimage, isUpperSet_empty, Relation.Fibration.isUpperSet_image, IsUpperSet.image, ClopenUpperSet.upper', isUpperSet_iInter, UpperSet.upper, IsLowerSet.toDual, Topology.IsScott.isOpen_iff_isUpperSet_and_dirSupInaccOn, isUpperSet_subtype_iff_isRelUpperSet, isUpperSet_sInter, IsUpperSet.prod, IsLowerSet.inv, IsUpperSet.cthickening', isUpperSet_sUnion, isUpperSet_univ, exists_isClopen_upper_or_lower_of_ne, Topology.IsLower.isUpperSet_of_isClosed, isUpperSet_iff_Ici_subset, IsUpperSet.erase, IsUpperSet.union, Topology.IsScott.isOpen_iff_isUpperSet_and_scottHausdorff_open, Relation.fibration_iff_isUpperSet_image_Ici, PriestleySpace.priestley, IsUpperSet.closure, HasUpperLowerClosure.isUpperSet_closure, isUpperSet_iff_Ioi_subset, Scott.IsOpen.isUpperSet, IsUpperSet.cthickening, Topology.WithUpperSet.isOpen_ofUpperSet_preimage, IsLowerSet.neg, isUpperSet_iUnion
LowerSet 📖	CompData	198 math math: LowerSet.iSup_Iic, LowerSet.mem_compl_iff, OrderEmbedding.supIrredLowerSet_apply, LowerSet.coe_eq_univ, LowerSet.map_Iio, LowerSet.inf_prod, lowerClosure_union, LowerSet.sup_prod, LowerSet.compl_map, LowerSet.erase_le, LowerSet.mem_iSup_iff, IsOpen.lowerClosure, LowerSet.compl_iInf, LowerSet.mem_inf_iff, LowerSet.coe_mk, UpperSet.compl_sup, lowerClosure_infs, LowerSet.coe_subset_coe, upperSetIsoLowerSet_apply, LowerSet.prod_mono, lowerClosure_eq_top_iff, LowerSet.prod_self_lt_prod_self, LowerSet.compl_iInf₂, subset_lowerClosure, LowerSet.sdiff_le_left, LowerSet.disjoint_coe, Topology.IsLowerSet.nhdsKer_eq_lowerClosure, lowerClosure_image, LowerSet.coe_sdiff, LowerSet.Iic_top, LowerSet.bot_prod, lowerClosure_one, LowerSet.Iio_strictMono, LowerSet.coe_map_apply, UpperSet.compl_sSup, LowerSet.bot_lt_Iic, LowerSet.Iio_bot, IsClosed.lowerClosure_pi, IsClopen.lowerClosure_pi, LowerSet.Iic_sup_erase, LowerSet.coe_eq_empty, LowerSet.Iic_iInf, lowerClosure_eq_bot_iff, LowerSet.coe_map, Order.Ideal.toLowerSet_injective, LowerSet.compl_iSup₂, Topology.IsScott.lowerClosure_subset_closure, lowerClosure_univ, lowerClosure_interior_subset', LowerSet.sdiff_eq_left, LowerSet.Iic_one, LowerSet.coe_Iio, Topology.IsUpper.isClosed_lowerClosure, LowerSet.total_le, OrderIso.supIrredLowerSet_symm_apply, lowerClosure_prod, LowerSet.prod_mono_left, LowerSet.coe_sSup, LowerSet.compl_inf, UpperSet.compl_iSup₂, LowerSet.Iic_injective, lowerClosure_empty, LowerSet.coe_iicsInfHom, LowerSet.coe_iSup, upperSetIsoLowerSet_symm_apply, LowerSet.sdiff_lt_left, LowerSet.symm_map, mem_lowerClosure, LowerSet.coe_ssubset_coe, LowerSet.coe_sub, LowerSet.supIrred_iff_of_finite, LowerSet.mem_top, LowerSet.coe_sup, LowerSet.lowerClosure_sup_sdiff, LowerSet.mem_iInf₂_iff, LowerSet.iicsInfHom_apply, LowerSet.coe_top, lowerClosure_eq_Iic_csSup, LowerSet.coe_map_symm_apply, lowerClosure_interior_subset, LowerSet.erase_sup_Iic, LowerSet.Iio_eq_bot, LowerSet.coe_sInf, LowerSet.Iic_strictMono, UpperSet.coe_compl, UpperSet.compl_iSup, LowerSet.disjoint_prod, Topology.IsUpperSet.closure_eq_lowerClosure, OrderIso.supIrredLowerSet_apply, LowerSet.coe_erase, UpperSet.compl_top, LowerSet.top_prod_top, lowerClosure_zero, LowerSet.compl_top, LowerSet.Iic_iInf₂, LowerSet.coe_inf, Order.Ideal.top_toLowerSet, LowerSet.coe_prod, LowerSet.Iic_le, LowerSet.coe_Iic, LowerSet.coe_iInf₂, LowerSet.coe_iInf, lowerClosure_add, LowerSet.iicInfHom_apply, OrderEmbedding.supIrredLowerSet_surjective, coe_lowerClosure, LowerSet.mem_iSup₂_iff, LowerSet.mem_map, lowerClosure_sUnion, IsAntichain.maximal_mem_lowerClosure_iff_mem, LowerSet.compl_le_compl, LowerSet.mem_Iio_iff, Matroid.setOf_indep_eq, IsLowerSet.lowerClosure, LowerSet.erase_lt, add_lowerClosure, LowerSet.compl_iSup, ordConnected_iff_upperClosure_inter_lowerClosure, upperBounds_lowerClosure, LowerSet.mem_Iic_iff, LowerSet.Iic_sInf, LowerSet.prod_mono_right, lowerClosure_iUnion, lowerClosure_le, lowerClosure_vadd, LowerSet.mem_sInf_iff, LowerSet.prod_self_le_prod_self, LowerSet.ext_iff, BddAbove.lowerClosure, LowerSet.prod_eq_bot, LowerSet.notMem_bot, LowerSet.prod_sup, LowerSet.prod_le_prod_iff, Set.OrdConnected.upperClosure_inter_lowerClosure, LowerSet.coe_compl, LowerSet.compl_sSup, IsUpperSet.disjoint_lowerClosure_left, LowerSet.prod_bot, LowerSet.map_refl, Set.Finite.lowerClosure, LowerSet.coe_add, LowerSet.coe_div, UpperSet.compl_map, UpperSet.compl_inf, OrderEmbedding.birkhoffSet_apply, LowerSet.prod_inf_prod, LowerSet.compl_sInf, LowerSet.coe_iicInfHom, lowerClosure_min, UpperSet.compl_iInf, LowerSet.Iic_prod, UpperSet.compl_bot, UpperSet.mem_compl_iff, LowerSet.map_Iic, lowerClosure_mul, LowerSet.coe_iSup₂, Finset.Colex.le_iff_sdiff_subset_lowerClosure, lowerClosure_smul, LowerSet.coe_nonempty, LowerSet.mem_mk, HasUpperLowerClosure.isOpen_lowerClosure, LowerSet.compl_bot, LowerSet.prod_inf, lowerClosure_eq_top, lowerClosure_mul_distrib, UpperSet.compl_iInf₂, mul_lowerClosure, Topology.IsLowerSet.nhdsSet_eq_principal_lowerClosure, UpperSet.coe_sdiff, UpperSet.compl_sInf, lowerClosure_add_distrib, LowerSet.lower, LowerSet.mem_prod, LowerSet.Ioi_le_Ici, gc_lowerClosure_coe, LowerSet.Iic_inf, LowerSet.lowerClosure, IsUpperSet.disjoint_lowerClosure_right, LowerSet.supIrred_Iic, Order.Ideal.coe_toLowerSet, LowerSet.carrier_eq_coe, lowerClosure_eq, LowerSet.Iic_zero, closure_lowerClosure_comm_pi, LowerSet.coe_bot, LowerSet.map_map, lowerClosure_mono, LowerSet.mem_sSup_iff, LowerSet.coe_mul, UpperSet.coe_erase, LowerSet.mem_iInf_iff, LowerSet.erase_eq, LowerSet.sdiff_sup_lowerClosure, LowerSet.compl_sup, bddAbove_lowerClosure, LowerSet.Ici_prod_Ici, LowerSet.mem_sup_iff, UpperSet.compl_le_compl
MaximalFor 📖	MathDef	14 math math: MaximalFor.anti, Set.Finite.exists_maximalFor, maximalFor_eq_iff, IntermediateField.exists_finset_maximalFor_isTranscendenceBasis_separableClosure, MinimalFor.maximalFor_of_strictAntiOn_comp, WeierstrassCurve.IsMinimal.val_Δ_maximal, WeierstrassCurve.isMinimal_iff, exists_maximalFor_of_wellFoundedGT, Set.Finite.exists_maximalFor', MaximalFor.of_strictMonoOn_comp, maximalFor_iff_forall_gt, Finset.exists_maximalFor, IntermediateField.FG.exists_finset_maximalFor_isTranscendenceBasis_separableClosure, maximalFor_id
MinimalFor 📖	MathDef	13 math math: MaximalFor.minimalFor_of_strictAntiOn_comp, MinimalFor.of_strictMonoOn_comp, exists_minimalFor_of_wellFoundedLT, MinimalFor.anti, Finset.exists_minimalFor, Function.isMinimalFor_argminOn, Function.isMinimalFor_argmin, Set.Finite.exists_minimalFor', Set.Finite.exists_minimalFor, Set.IsPWO.exists_minimalFor, minimalFor_id, minimalFor_eq_iff, minimalFor_iff_forall_lt
RelLowerSet 📖	CompData	1 math math: RelLowerSet.isRelLowerSet
RelUpperSet 📖	CompData	1 math math: RelUpperSet.isRelUpperSet
Total 📖	MathDef	—
UpperSet 📖	CompData	216 math math: UpperSet.mem_Ioi_iff, UpperSet.coe_Ici, UpperSet.erase_eq, upperClosure_zero, LowerSet.mem_compl_iff, upperClosure_one, UpperSet.Ici_injective, UpperSet.Ici_inf_erase, UpperSet.coe_one, ClopenUpperSet.coe_toUpperSet, LowerSet.compl_map, upperClosure_eq, UpperSet.mem_inf_iff, LowerSet.compl_iInf, UpperSet.Ici_zero, BddBelow.upperClosure, FiniteArchimedeanClass.mem_addSubgroup_iff, UpperSet.compl_sup, MulArchimedeanClass.subgroup_strictAntiOn, UpperSet.mem_sInf_iff, bddBelow_upperClosure, ArchimedeanClass.addSubgroup_antitone, Topology.IsUpperSet.nhdsKer_eq_upperClosure, upperClosure_image, upperSetIsoLowerSet_apply, OrderEmbedding.infIrredUpperSet_surjective, UpperSet.sdiff_eq_left, LowerSet.compl_iInf₂, UpperSet.coe_add, IsClosed.upperClosure, UpperSet.carrier_eq_coe, IsUpperSet.upperClosure, LowerSet.coe_sdiff, UpperSet.Ici_lt_top, UpperSet.mem_iSup_iff, IsClopen.upperClosure_pi, UpperSet.mem_map, UpperSet.map_map, UpperSet.compl_sSup, upperClosure_sups, Topology.IsLowerSet.closure_eq_upperClosure, UpperSet.coe_inf, subset_upperClosure, UpperSet.coe_ssubset_coe, add_upperClosure, UpperSet.ext_iff, UpperSet.coe_eq_empty, upperClosure_interior_subset', UpperSet.coe_map_apply, OrderIso.infIrredUpperSet_symm_apply, UpperSet.Ici_iSup, UpperSet.coe_div, MulArchimedeanClass.mem_subgroup_iff, MulArchimedeanClass.subsemigroup_strictAnti, LowerSet.compl_iSup₂, UpperSet.Ioi_top, UpperSet.codisjoint_coe, upperClosure_interior_subset, UpperSet.mem_sup_iff, UpperSet.prod_le_prod_iff, UpperSet.Ici_sup, UpperSet.notMem_top, UpperSet.coe_prod, LowerSet.compl_inf, UpperSet.compl_iSup₂, UpperSet.map_refl, UpperSet.prod_top, UpperSet.Ici_sSup, UpperSet.top_prod, Topology.IsLower.isClosed_upperClosure, upperSetIsoLowerSet_symm_apply, UpperSet.mem_Ici_iff, UpperSet.coe_mk, UpperSet.symm_map, OrderEmbedding.infIrredUpperSet_apply, PrimitiveSpectrum.hull_finsetInf, upperClosure_mul, UpperSet.Ici_prod_Ici, UpperSet.prod_mono_left, closure_upperClosure_comm_pi, UpperSet.coe_iciSupHom, UpperSet.infIrred_Ici, lowerBounds_upperClosure, UpperSet.Ioi_eq_top, UpperSet.coe_iInf₂, UpperSet.mem_sSup_iff, UpperSet.coe_eq_univ, UpperSet.coe_compl, UpperSet.sup_prod, UpperSet.compl_iSup, UpperSet.le_Ici, FiniteArchimedeanClass.subsemigroup_eq_addSubgroup, UpperSet.erase_inf_Ici, upperClosure_min, LowerSet.coe_erase, upperClosure_eq_top_iff, ArchimedeanClass.mem_addSubgroup_iff, UpperSet.compl_top, UpperSet.mem_iInf_iff, ArchimedeanClass.addSubgroup_eq_bot, UpperSet.map_Ici, UpperSet.coe_mul, IsAntichain.minimal_mem_upperClosure_iff_mem, LowerSet.compl_top, UpperSet.coe_icisSupHom, UpperSet.lt_sdiff_left, UpperSet.upperClosure, UpperSet.Ici_one, IsOpen.upperClosure, LowerSet.compl_le_compl, UpperSet.coe_zero, Topology.IsUpperSet.nhdsSet_eq_principal_upperClosure, PrimitiveSpectrum.preimage_upperClosure_compl_finset, ArchimedeanClass.subsemigroup_strictAnti, upperClosure_empty, gc_upperClosure_coe, UpperSet.coe_top, UpperSet.icisSupHom_apply, upperClosure_prod, UpperSet.prod_inf, UpperSet.coe_iSup, UpperSet.mem_iSup₂_iff, LowerSet.compl_iSup, FiniteMulArchimedeanClass.mem_subgroup_iff, UpperSet.prod_mono, UpperSet.iciSupHom_apply, ordConnected_iff_upperClosure_inter_lowerClosure, OrderIso.infIrredUpperSet_apply, UpperSet.prod_self_le_prod_self, upperClosure_univ, UpperSet.mem_mk, upperClosure_eq_bot_iff, UpperSet.le_erase, UpperSet.coe_iInf, UpperSet.prod_self_lt_prod_self, IsLowerSet.disjoint_upperClosure_left, UpperSet.coe_sub, upperClosure_add_distrib, IsLowerSet.disjoint_upperClosure_right, HasUpperLowerClosure.isOpen_upperClosure, UpperSet.upperClosure_inf_sdiff, UpperSet.coe_iSup₂, upperClosure_sUnion, UpperSet.coe_nonempty, UpperSet.map_Ioi, UpperSet.mem_prod, coe_upperClosure, UpperSet.coe_sup, FiniteArchimedeanClass.addSubgroup_strictAnti, upperClosure_add, UpperSet.sdiff_inf_upperClosure, Set.OrdConnected.upperClosure_inter_lowerClosure, LowerSet.coe_compl, LowerSet.compl_sSup, UpperSet.Ioi_strictMono, upperClosure_vadd, FiniteMulArchimedeanClass.subgroup_eq_bot, le_upperClosure, UpperSet.upper, UpperSet.infIrred_iff_of_finite, MulArchimedeanClass.subgroup_antitone, UpperSet.compl_map, UpperSet.compl_inf, LowerSet.compl_sInf, ArchimedeanClass.addSubgroup_strictAntiOn, FiniteArchimedeanClass.submodule_strictAnti, UpperSet.compl_iInf, UpperSet.coe_map, UpperSet.coe_Ioi, UpperSet.compl_bot, FiniteMulArchimedeanClass.subsemigroup_eq_subgroup, UpperSet.mem_compl_iff, UpperSet.bot_prod_bot, upperClosure_mul_distrib, UpperSet.coe_sInf, UpperSet.Ici_le_Ioi, LowerSet.compl_bot, upperClosure_iUnion, UpperSet.prod_sup_prod, UpperSet.le_sdiff_left, UpperSet.prod_mono_right, UpperSet.Ici_bot, mul_upperClosure, UpperSet.compl_iInf₂, UpperSet.coe_sSup, UpperSet.coe_sdiff, Set.Finite.upperClosure, UpperSet.codisjoint_prod, UpperSet.compl_sInf, UpperSet.coe_subset_coe, FiniteMulArchimedeanClass.subgroup_strictAnti, IsClosed.upperClosure_pi, UpperSet.inf_prod, MulArchimedeanClass.subgroup_eq_bot, upperClosure_union, UpperSet.coe_map_symm_apply, UpperSet.lt_erase, UpperSet.total_le, UpperSet.mem_iInf₂_iff, FiniteArchimedeanClass.addSubgroup_eq_bot, UpperSet.coe_bot, UpperSet.prod_eq_top, upperClosure_smul, UpperSet.coe_erase, UpperSet.Ici_prod, UpperSet.mem_bot, mem_upperClosure, upperClosure_eq_Ici_csInf, upperClosure_eq_bot, LowerSet.compl_sup, UpperSet.iInf_Ici, UpperSet.prod_sup, upperClosure_anti, UpperSet.compl_le_compl, UpperSet.Ici_iSup₂, UpperSet.Ici_strictMono
instTransOfIsTrans 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antisymm 📖	—	—	—	—	—
antisymm' 📖	—	—	—	—	antisymm
antisymm_iff 📖	—	—	—	—	antisymm refl
antisymm_of 📖	—	—	—	—	antisymm
antisymm_of' 📖	—	—	—	—	antisymm'
asymm 📖	—	—	—	—	—
asymm_of 📖	—	—	—	—	asymm
asymm_of_isTrans_of_irrefl 📖	—	—	—	—	trans irrefl
comm 📖	—	—	—	—	symm
comm_of 📖	—	—	—	—	comm
empty_relation_apply 📖	—	—	—	—	—
eq_isEquiv 📖	mathematical	—	IsEquiv	—	—
extensional_of_trichotomous_of_irrefl 📖	—	—	—	—	trichotomous irrefl
iff_isEquiv 📖	mathematical	—	IsEquiv	—	—
instIrreflEmptyRelation_mathlib 📖	—	—	—	—	—
instIsTransOfTrans 📖	mathematical	—	IsTrans	—	—
irrefl 📖	—	—	—	—	—
irrefl_of 📖	—	—	—	—	irrefl
isTrans_def 📖	mathematical	—	IsTrans	—	IsTrans.trans
ne_of_irrefl 📖	—	—	—	—	irrefl
ne_of_irrefl' 📖	—	—	—	—	irrefl
not_rel_of_subsingleton 📖	—	—	—	—	irrefl
of_eq 📖	—	—	—	—	refl
refl 📖	—	—	—	—	—
refl_of 📖	—	—	—	—	refl
rel_congr 📖	—	—	—	—	rel_congr_left rel_congr_right
rel_congr_left 📖	—	—	—	—	trans_of symm_of
rel_congr_right 📖	—	—	—	—	trans_of symm_of
rel_of_subsingleton 📖	—	—	—	—	refl
symm_of 📖	—	—	—	—	symm
total_of 📖	—	—	—	—	—
trans 📖	—	—	—	—	IsTrans.trans
trans_of 📖	—	—	—	—	trans
trans_trichotomous_left 📖	—	—	—	—	trichotomous_of trans
trans_trichotomous_right 📖	—	—	—	—	trichotomous_of trans
transitive_of_trans 📖	mathematical	—	Transitive	—	IsTrans.trans
trichotomous 📖	—	—	—	—	—
trichotomous_of 📖	—	—	—	—	trichotomous

---

← Back to Index