OrdConnectedLinear

📁 Source: Mathlib/Order/Interval/Set/OrdConnectedLinear.lean

Statistics

Metric	Count
Definitions	0
Theorems eq_Icc_iff_int, eq_Icc_iff_nat, ordConnected_iff_of_bdd, ordConnected_iff_of_bdd', ordConnected_iff_disjoint_Ioo_empty	5
Total	5

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ordConnected_iff_disjoint_Ioo_empty 📖	mathematical	—	OrdConnected PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioo Set instEmptyCollection	—	OrdConnected.out mem_Icc_of_Ioo ext ordConnected_of_Ioo Finite.exists_le_maximal Finite.inter_of_right finite_Icc le_refl LT.lt.le lt_of_le_of_ne Finite.exists_le_minimal lt_of_le_of_ne' Maximal.not_gt le_trans Minimal.not_lt Ioc_union_Ico_eq_Ioo eq_empty_iff_forall_notMem Maximal.prop Minimal.prop

Set.Nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_Icc_iff_int 📖	mathematical	Set.Nonempty BddBelow BddAbove	Set.Icc PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet	—	ordConnected_iff_of_bdd instNoMaxOrderOfNontrivial IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing Int.instNontrivial
eq_Icc_iff_nat 📖	mathematical	Set.Nonempty BddAbove	Set.Icc Nat.instPreorder InfSet.sInf Nat.instInfSet SupSet.sSup Nat.instSupSet	—	ordConnected_iff_of_bdd OrderBot.bddBelow Nat.instNoMaxOrder
ordConnected_iff_of_bdd 📖	mathematical	Set.Nonempty BddBelow Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice BddAbove	Set.OrdConnected Set.Icc InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet	—	BddBelow.finite_of_bddAbove le_antisymm subset_Icc_csInf_csSup Set.Icc_subset csInf_mem csSup_mem Set.ordConnected_Icc
ordConnected_iff_of_bdd' 📖	mathematical	Set.Nonempty	Set.OrdConnected PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Set.Icc InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet	—	ordConnected_iff_of_bdd OrderBot.bddBelow OrderTop.bddAbove

---

← Back to Index