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 reflexive, symmetric, transitive, irrefl, irreflexive, 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, 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	87
Total	121

Equivalence

Theorems

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

InvImage

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
irrefl 📖	—	—	—	—	—
irreflexive 📖	—	—	—	—	irrefl
trans 📖	—	Transitive	—	—	—

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	10 math math: IsConjRoot.instIsEquiv, LocalizedModule.r.isEquiv, SetTheory.PGame.instIsEquivEquiv, eq_isEquiv, Order.Preimage.instIsEquiv, Quotient.instIsEquivEquiv, SetTheory.PGame.instIsEquivIdentical, Ne.instIsEquiv_compl, iff_isEquiv, Path.Homotopic.instIsEquiv
IsIrrefl 📖	MathDef	—
IsLinearOrder 📖	CompData	4 math math: extend_partialOrder, RelEmbedding.isLinearOrder, instIsLinearOrderGe, instIsLinearOrderLe
IsLowerSet 📖	MathDef	47 math math: Order.IsIdeal.IsLowerSet, IsUpperSet.ofDual, PrincipalSeg.isLowerSet_range, Topology.IsLowerSet.isOpen_iff_isLowerSet, IsUpperSet.compl, Order.Ideal.lower, isUpperSet_preimage_toDual_iff, isLowerSet_iff_Iic_subset, Topology.IsScott.isClosed_iff_isLowerSet_and_dirSupClosed, isLowerSet_univ, Relation.fibration_iff_isLowerSet_image, isLowerSet_preimage_toDual_iff, Topology.IsUpper.isLowerSet_of_isClosed, isLowerSet_Iio, Topology.WithLowerSet.isLowerSet_toLowerSet_preimage, IsUpperSet.neg, YoungDiagram.isLowerSet, isLowerSet_preimage_ofDual_iff, IsUpperSet.sub_left, Topology.IsUpperSet.isClosed_iff_isLower, 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, Order.isIdeal_iff, Topology.WithLowerSet.isOpen_ofLowerSet_preimage, Finset.shatterer_eq, Topology.IsScott.isLowerSet_of_isClosed, isLowerSet_iff_forall_lt, Topology.IsLower.isLowerSet_of_isOpen, isLowerSet_iff_Iio_subset, isLowerSet_empty, IsUpperSet.toDual, exists_isClopen_upper_or_lower_of_ne, Relation.fibration_iff_isLowerSet_image_Iic, IsUpperSet.isLowerSet_preimage_coe, LowerSet.lower', exists_isClopen_lower_of_not_le, LowerSet.lower, lowerClosure_eq, InitialSeg.isLowerSet_range, isLowerSet_Iic
IsPartialOrder 📖	CompData	9 math math: IsLinearOrder.toIsPartialOrder, List.instIsPartialOrderIsPrefix, RelEmbedding.isPartialOrder, List.instIsPartialOrderIsInfix, instIsPartialOrderSetIsExtreme, List.instIsPartialOrderIsSuffix, IsPartialOrder.swap, instIsPartialOrderLe, instIsPartialOrderGe
IsPreorder 📖	CompData	9 math math: IsPreorder.swap, instIsPreorderPFunNatTuringReducible, instIsPreorderLe, IsEquiv.toIsPreorder, Order.Preimage.instIsPreorder, IsPartialOrder.toIsPreorder, Subrel.instIsPreorderSubtype, instIsPreorderGe, RelEmbedding.isPreorder
IsRefl 📖	MathDef	—
IsRelLowerSet 📖	MathDef	8 math math: isRelLowerSet_Icc_ge, Geometry.SimplicialComplex.isRelLowerSet_faces, IsLowerSet.isRelLowerSet_sep, isRelLowerSet_empty, RelLowerSet.isRelLowerSet, isLowerSet_subtype_iff_isRelLowerSet, isRelLowerSet_self, RelLowerSet.isRelLowerSet'
IsRelUpperSet 📖	MathDef	7 math math: isRelUpperSet_empty, IsUpperSet.isRelUpperSet_sep, RelUpperSet.isRelUpperSet', isRelUpperSet_Icc_le, isUpperSet_subtype_iff_isRelUpperSet, RelUpperSet.isRelUpperSet, 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	1 math math: PartENat.isTotal
IsTrans 📖	CompData	40 math math: instIsTransAntisymmRel, Associated.instIsTrans, instIsTransDvd, instIsTransOfTrans, Finset.instIsTransSubset, Quotient.instIsTransLe, List.SublistForall₂.is_trans, OrderDual.instIsTransLE, SetTheory.PGame.instIsTransIdentical, FirstOrder.Language.Theory.Iff.instIsTransBoundedFormula, IsStrictOrder.toIsTrans, Finset.instIsTransSSubset, Set.instIsTransSubset, IsPreorder.toIsTrans, PSet.instIsTransSubset, IsTrans.decide, RelEmbedding.isTrans, ZFSet.IsOrdinal.isTrans, instIsTransGt, instIsTransLe, FirstOrder.Language.Theory.Imp.instIsTransBoundedFormula, ZFSet.isOrdinal_iff_isTrans, instIsTransLt, Sum.instIsTransLiftRel, IsTrans.swap, Subrel.instIsTransSubtype, Prod.instIsTransLex, instIsTransGe, AddCommGroup.instIsTransModEq, SetTheory.PGame.instIsTransSubsequent, ZFSet.instIsTransSubset, IsWellOrder.toIsTrans, instIsTransNatLeHAddOfNat, Set.instIsTransSSubset, Sum.instIsTransLex, Relation.instIsTransTransGen, OrderDual.instIsTransLT, Int.ModEq.instIsTrans, Relation.instIsTransReflTransGen, Order.Preimage.instIsTrans
IsTrichotomous 📖	MathDef	—
IsUpperSet 📖	MathDef	49 math math: UpperSet.upper', Topology.IsScott.isUpperSet_of_isOpen, IsLowerSet.div_left, isUpperSet_iff_forall_lt, upperClosure_eq, IsLowerSet.ofDual, Set.Intersecting.isUpperSet, Set.Intersecting.isUpperSet', isUpperSet_preimage_toDual_iff, Specialization.isOpen_toEquiv_preimage, IsLowerSet.sub_left, isLowerSet_preimage_toDual_iff, Topology.IsUpperSet.isOpen_iff_isUpperSet, exists_isClopen_upper_of_not_le, isUpperSet_Ioi, Topology.IsLowerSet.isClosed_iff_isUpper, Relation.fibration_iff_isUpperSet_image, IsLowerSet.compl, Topology.WithUpperSet.isUpperSet_toUpperSet_preimage, Topology.WithScott.isOpen_iff_isUpperSet_and_scottHausdorff_open', isUpperSet_Ici, isLowerSet_preimage_ofDual_iff, ClopenUpperSet.upper, Set.monotone_mem, isLowerSet_compl, isUpperSet_preimage_ofDual_iff, Topology.IsUpper.isUpperSet_of_isOpen, isUpperSet_compl, IsLowerSet.isUpperSet_preimage_coe, isUpperSet_setOf, Specialization.isUpperSet_ofEquiv_preimage, isUpperSet_empty, ClopenUpperSet.upper', UpperSet.upper, IsLowerSet.toDual, Topology.IsScott.isOpen_iff_isUpperSet_and_dirSupInaccOn, isUpperSet_subtype_iff_isRelUpperSet, IsLowerSet.inv, isUpperSet_univ, exists_isClopen_upper_or_lower_of_ne, Topology.IsLower.isUpperSet_of_isClosed, isUpperSet_iff_Ici_subset, Topology.IsScott.isOpen_iff_isUpperSet_and_scottHausdorff_open, Relation.fibration_iff_isUpperSet_image_Ici, PriestleySpace.priestley, isUpperSet_iff_Ioi_subset, Scott.IsOpen.isUpperSet, Topology.WithUpperSet.isOpen_ofUpperSet_preimage, IsLowerSet.neg
LowerSet 📖	CompData	189 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, 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, UpperSet.compl_sSup, LowerSet.bot_lt_Iic, LowerSet.Iio_bot, IsClosed.lowerClosure_pi, IsClopen.lowerClosure_pi, 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.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.mem_iInf₂_iff, LowerSet.iicsInfHom_apply, LowerSet.coe_top, lowerClosure_eq_Iic_csSup, lowerClosure_interior_subset, 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, 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, LowerSet.instIsConcreteLE, 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, 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.compl_sup, bddAbove_lowerClosure, LowerSet.Ici_prod_Ici, LowerSet.mem_sup_iff, UpperSet.compl_le_compl
MaximalFor 📖	MathDef	12 math math: 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_iff_forall_gt, Finset.exists_maximalFor, IntermediateField.FG.exists_finset_maximalFor_isTranscendenceBasis_separableClosure, maximalFor_id
MinimalFor 📖	MathDef	11 math math: MaximalFor.minimalFor_of_strictAntiOn_comp, exists_minimalFor_of_wellFoundedLT, 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	207 math math: UpperSet.mem_Ioi_iff, UpperSet.coe_Ici, UpperSet.erase_eq, upperClosure_zero, LowerSet.mem_compl_iff, upperClosure_one, UpperSet.Ici_injective, 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', 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, 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, 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.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.coe_iSup₂, upperClosure_sUnion, UpperSet.coe_nonempty, UpperSet.map_Ioi, UpperSet.mem_prod, coe_upperClosure, UpperSet.coe_sup, FiniteArchimedeanClass.addSubgroup_strictAnti, upperClosure_add, 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.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.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
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