LinearOrder

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

Statistics

Metric	Count
Definitions LinearOrder	1
Theorems Icc_subset_Icc_union_Icc, Icc_subset_Icc_union_Ioc, Icc_subset_Ico_union_Icc, Icc_union_Icc, Icc_union_Icc', Icc_union_Icc_eq_Icc, Icc_union_Ici, Icc_union_Ici', Icc_union_Ici_eq_Ici, Icc_union_Ico_eq_Ico, Icc_union_Ioc_eq_Icc, Icc_union_Ioi_eq_Ici, Icc_union_Ioo_eq_Ico, Ici_diff_Ici, Ici_diff_Ioi, Ici_eq_singleton_iff_isTop, Ici_subset_Icc_union_Ici, Ici_subset_Icc_union_Ioi, Ici_subset_Ico_union_Ici, Ici_union_Iic, Ici_union_Iic_of_le, Ici_union_Iio, Ici_union_Iio_of_le, Ico_diff_Iio, Ico_eq_Ico_iff, Ico_inter_Ico, Ico_inter_Iio, Ico_subset_Icc_union_Ico, Ico_subset_Icc_union_Ioo, Ico_subset_Ico_iff, Ico_subset_Ico_union_Ico, Ico_union_Icc_eq_Icc, Ico_union_Ici, Ico_union_Ici', Ico_union_Ici_eq_Ici, Ico_union_Ico, Ico_union_Ico', Ico_union_Ico_eq_Ico, Iic_diff_Iic, Iic_diff_Iio, Iic_diff_Ioc, Iic_diff_Ioc_self_of_le, Iic_eq_singleton_iff_isBot, Iic_subset_Iic_union_Icc, Iic_subset_Iic_union_Ioc, Iic_subset_Iio_union_Icc, Iic_union_Icc, Iic_union_Icc', Iic_union_Icc_eq_Iic, Iic_union_Ici, Iic_union_Ici_of_le, Iic_union_Ico_eq_Iio, Iic_union_Ioc, Iic_union_Ioc', Iic_union_Ioc_eq_Iic, Iic_union_Ioi, Iic_union_Ioi_of_le, Iic_union_Ioo_eq_Iio, Iio_diff_Iic, Iio_diff_Iio, Iio_inj, Iio_injective, Iio_inter_Iio, Iio_inter_Ioo, Iio_ssubset_Iio_iff, Iio_subset_Iic_iff, Iio_subset_Iic_union_Ico, Iio_subset_Iic_union_Ioo, Iio_subset_Iio_iff, Iio_subset_Iio_union_Ico, Iio_union_Icc_eq_Iic, Iio_union_Ici, Iio_union_Ici_of_le, Iio_union_Ico, Iio_union_Ico', Iio_union_Ico_eq_Iio, Iio_union_Ioi, Iio_union_Ioi_of_lt, Iio_union_Ioo, Iio_union_Ioo', Ioc_diff_Iic, Ioc_diff_Ioi, Ioc_eq_Ioc_iff, Ioc_inter_Ioc, Ioc_inter_Ioi, Ioc_inter_Ioo_of_left_lt, Ioc_inter_Ioo_of_right_le, Ioc_subset_Ioc_iff, Ioc_subset_Ioc_union_Icc, Ioc_subset_Ioc_union_Ioc, Ioc_subset_Ioo_union_Icc, Ioc_union_Icc_eq_Ioc, Ioc_union_Ici_eq_Ioi, Ioc_union_Ico_eq_Ioo, Ioc_union_Ioc, Ioc_union_Ioc', Ioc_union_Ioc_eq_Ioc, Ioc_union_Ioc_left, Ioc_union_Ioc_right, Ioc_union_Ioc_symm, Ioc_union_Ioc_union_Ioc_cycle, Ioc_union_Ioi, Ioc_union_Ioi', Ioc_union_Ioi_eq_Ioi, Ioc_union_Ioo_eq_Ioo, Ioi_diff_Ici, Ioi_diff_Ioc, Ioi_diff_Ioi, Ioi_inj, Ioi_injective, Ioi_inter_Ioi, Ioi_inter_Ioo, Ioi_ssubset_Ioi_iff, Ioi_subset_Ici_iff, Ioi_subset_Ioc_union_Ici, Ioi_subset_Ioc_union_Ioi, Ioi_subset_Ioi_iff, Ioi_subset_Ioo_union_Ici, Ioi_union_Iic, Ioi_union_Iic_of_le, Ioi_union_Iio, Ioi_union_Iio_of_lt, Ioo_inter_Iio, Ioo_inter_Ioc_of_left_le, Ioo_inter_Ioc_of_right_lt, Ioo_inter_Ioi, Ioo_inter_Ioo, Ioo_subset_Ioc_union_Ico, Ioo_subset_Ioc_union_Ioo, Ioo_subset_Ioo_iff, Ioo_subset_Ioo_union_Ico, Ioo_subset_Ioo_union_Ioo, Ioo_union_Icc_eq_Ioc, Ioo_union_Ici_eq_Ioi, Ioo_union_Ico_eq_Ioo, Ioo_union_Ioi, Ioo_union_Ioi', Ioo_union_Ioo, Ioo_union_Ioo', compl_Ici, compl_Iic, compl_Iio, compl_Ioc, compl_Ioi, notMem_Ici, notMem_Iic, notMem_Iio, notMem_Ioi	148
Total	149

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Icc_subset_Icc_union_Icc 📖	mathematical	—	Set instHasSubset Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instUnion	—	Subset.trans Icc_subset_Icc_union_Ioc union_subset_union_right Ioc_subset_Icc_self
Icc_subset_Icc_union_Ioc 📖	mathematical	—	Set instHasSubset Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instUnion Ioc	—	le_or_gt
Icc_subset_Ico_union_Icc 📖	mathematical	—	Set instHasSubset Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instUnion Ico	—	lt_or_ge
Icc_union_Icc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	Set instUnion Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Icc_union_Icc' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Icc_union_Icc_eq_Icc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Subset.antisymm LE.le.trans Icc_subset_Icc_union_Icc
Icc_union_Ici 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup	Set instUnion Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ici SemilatticeInf.toMin	—	—
Icc_union_Ici' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ici SemilatticeInf.toMin	—	Icc_union_Ici LE.le.trans le_max_right
Icc_union_Ici_eq_Ici 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ici	—	Subset.antisymm LE.le.trans Ici_subset_Icc_union_Ici
Icc_union_Ico_eq_Ico 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	Set instUnion Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ico	—	Subset.antisymm LE.le.trans_lt LE.le.trans Ico_subset_Icc_union_Ico
Icc_union_Ioc_eq_Icc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioc	—	Subset.antisymm LE.le.trans LT.lt.le Icc_subset_Icc_union_Ioc
Icc_union_Ioi_eq_Ici 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioi Ici	—	Subset.antisymm LE.le.trans le_of_lt Ici_subset_Icc_union_Ioi
Icc_union_Ioo_eq_Ico 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	Set instUnion Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioo Ico	—	Subset.antisymm LE.le.trans_lt LE.le.trans LT.lt.le Ico_subset_Icc_union_Ioo
Ici_diff_Ici 📖	mathematical	—	Set instSDiff Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ico	—	diff_eq compl_Ici Ici_inter_Iio
Ici_diff_Ioi 📖	mathematical	—	Set instSDiff Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioi Icc	—	diff_eq compl_Ioi Ici_inter_Iic
Ici_eq_singleton_iff_isTop 📖	mathematical	—	Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set instSingletonSet IsTop Preorder.toLE	—	LT.lt.le lt_irrefl LE.le.trans_lt Eq.le mem_singleton_iff ext LE.le.ge_iff_eq
Ici_subset_Icc_union_Ici 📖	mathematical	—	Set instHasSubset Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instUnion Icc	—	Subset.trans Ici_subset_Ico_union_Ici union_subset_union_left Ico_subset_Icc_self
Ici_subset_Icc_union_Ioi 📖	mathematical	—	Set instHasSubset Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instUnion Icc Ioi	—	le_or_gt
Ici_subset_Ico_union_Ici 📖	mathematical	—	Set instHasSubset Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instUnion Ico	—	lt_or_ge
Ici_union_Iic 📖	mathematical	—	Set instUnion Ici PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Iic univ	—	Ici_union_Iic_of_le le_rfl
Ici_union_Iic_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Ici PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Iic univ	—	eq_univ_of_forall LE.le.le_or_ge
Ici_union_Iio 📖	mathematical	—	Set instUnion Ici PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Iio univ	—	Ici_union_Iio_of_le le_rfl
Ici_union_Iio_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Ici PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Iio univ	—	eq_univ_of_forall LE.le.lt_or_ge
Ico_diff_Iio 📖	mathematical	—	Set instSDiff Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Iio SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Ico_eq_Ico_iff 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Ico_subset_Ico_iff Eq.subset instReflSubset Eq.superset
Ico_inter_Ico 📖	mathematical	—	Set instInter Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup SemilatticeInf.toMin	—	—
Ico_inter_Iio 📖	mathematical	—	Set instInter Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Iio SemilatticeInf.toMin	—	—
Ico_subset_Icc_union_Ico 📖	mathematical	—	Set instHasSubset Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instUnion Icc	—	Subset.trans Ico_subset_Icc_union_Ioo union_subset_union_right Ioo_subset_Ico_self
Ico_subset_Icc_union_Ioo 📖	mathematical	—	Set instHasSubset Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instUnion Icc Ioo	—	le_or_gt
Ico_subset_Ico_iff 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instHasSubset Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE	—	le_rfl le_of_not_gt lt_irrefl LT.lt.le Ico_subset_Ico
Ico_subset_Ico_union_Ico 📖	mathematical	—	Set instHasSubset Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instUnion	—	lt_or_ge
Ico_union_Icc_eq_Icc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Icc	—	Subset.antisymm LE.le.trans LT.lt.le Icc_subset_Ico_union_Icc
Ico_union_Ici 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup	Set instUnion Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ici SemilatticeInf.toMin	—	—
Ico_union_Ici' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ici SemilatticeInf.toMin	—	Ico_union_Ici LE.le.trans le_max_right
Ico_union_Ici_eq_Ici 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ici	—	Subset.antisymm LE.le.trans Ici_subset_Ico_union_Ici
Ico_union_Ico 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	Set instUnion Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Ico_union_Ico' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	—	Ico_union_Ico LE.le.trans min_le_left le_max_right
Ico_union_Ico_eq_Ico 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Subset.antisymm LT.lt.trans_le LE.le.trans Ico_subset_Ico_union_Ico
Iic_diff_Iic 📖	mathematical	—	Set instSDiff Iic PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioc	—	diff_eq compl_Iic Iic_inter_Ioi
Iic_diff_Iio 📖	mathematical	—	Set instSDiff Iic PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Iio Icc	—	diff_eq compl_Iio Iic_inter_Ici
Iic_diff_Ioc 📖	mathematical	—	Set instSDiff Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioc SemilatticeInf.toMin	—	—
Iic_diff_Ioc_self_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instSDiff Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioc	—	—
Iic_eq_singleton_iff_isBot 📖	mathematical	—	Iic PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Set instSingletonSet IsBot Preorder.toLE	—	LT.lt.le not_le lt_irrefl LE.le.trans_lt' Eq.ge mem_singleton_iff ext mem_Iic LE.le.ge_iff_eq'
Iic_subset_Iic_union_Icc 📖	mathematical	—	Set instHasSubset Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instUnion Icc	—	Subset.trans Iic_subset_Iic_union_Ioc union_subset_union_right Ioc_subset_Icc_self
Iic_subset_Iic_union_Ioc 📖	mathematical	—	Set instHasSubset Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instUnion Ioc	—	le_or_gt
Iic_subset_Iio_union_Icc 📖	mathematical	—	Set instHasSubset Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instUnion Iio Icc	—	lt_or_ge
Iic_union_Icc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin	Set instUnion Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Icc SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Iic_union_Icc' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Icc SemilatticeSup.toMax Lattice.toSemilatticeSup	—	Iic_union_Icc LE.le.trans min_le_left
Iic_union_Icc_eq_Iic 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Icc	—	Subset.antisymm le_trans Iic_subset_Iic_union_Icc
Iic_union_Ici 📖	mathematical	—	Set instUnion Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ici univ	—	Iic_union_Ici_of_le le_rfl
Iic_union_Ici_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ici univ	—	eq_univ_of_forall LE.le.ge_or_le
Iic_union_Ico_eq_Iio 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ico Iio	—	Subset.antisymm lt_of_le_of_lt Iio_subset_Iic_union_Ico
Iic_union_Ioc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin	Set instUnion Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioc SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Iic_union_Ioc' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioc SemilatticeSup.toMax Lattice.toSemilatticeSup	—	Iic_union_Ioc LE.le.trans_lt min_le_left
Iic_union_Ioc_eq_Iic 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioc	—	Subset.antisymm le_trans Iic_subset_Iic_union_Ioc
Iic_union_Ioi 📖	mathematical	—	Set instUnion Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioi univ	—	Iic_union_Ioi_of_le le_rfl
Iic_union_Ioi_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioi univ	—	eq_univ_of_forall LE.le.gt_or_le
Iic_union_Ioo_eq_Iio 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioo Iio	—	Subset.antisymm lt_of_le_of_lt Iio_subset_Iic_union_Ioo
Iio_diff_Iic 📖	mathematical	—	Set instSDiff Iio PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Iic Ioo	—	diff_eq compl_Iic Iio_inter_Ioi
Iio_diff_Iio 📖	mathematical	—	Set instSDiff Iio PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Ico	—	diff_eq compl_Iio Iio_inter_Ici
Iio_inj 📖	mathematical	—	Iio PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Iio_injective
Iio_injective 📖	mathematical	—	Set Iio PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	eq_of_forall_lt_iff ext_iff
Iio_inter_Iio 📖	mathematical	—	Set instInter Iio PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin Lattice.toSemilatticeInf	—	ext lt_inf_iff
Iio_inter_Ioo 📖	mathematical	—	Set instInter Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioo SemilatticeInf.toMin	—	—
Iio_ssubset_Iio_iff 📖	mathematical	—	Set instHasSSubset Iio PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	—	ssubset_iff_exists LT.lt.trans_le' le_of_not_gt Iio_ssubset_Iio
Iio_subset_Iic_iff 📖	mathematical	—	Set instHasSubset Iio PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Iic Preorder.toLE	—	exists_between' not_le lt_irrefl LT.lt.trans_le' Iio_subset_Iic
Iio_subset_Iic_union_Ico 📖	mathematical	—	Set instHasSubset Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instUnion Iic Ico	—	Subset.trans Iio_subset_Iic_union_Ioo union_subset_union_right Ioo_subset_Ico_self
Iio_subset_Iic_union_Ioo 📖	mathematical	—	Set instHasSubset Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instUnion Iic Ioo	—	le_or_gt
Iio_subset_Iio_iff 📖	mathematical	—	Set instHasSubset Iio PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE	—	lt_irrefl not_le Iio_subset_Iio
Iio_subset_Iio_union_Ico 📖	mathematical	—	Set instHasSubset Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instUnion Ico	—	lt_or_ge
Iio_union_Icc_eq_Iic 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Icc Iic	—	Subset.antisymm LE.le.trans le_of_lt Iic_subset_Iio_union_Icc
Iio_union_Ici 📖	mathematical	—	Set instUnion Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ici univ	—	Iio_union_Ici_of_le le_rfl
Iio_union_Ici_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ici univ	—	eq_univ_of_forall LE.le.ge_or_lt
Iio_union_Ico 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin	Set instUnion Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ico SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Iio_union_Ico' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ico SemilatticeSup.toMax Lattice.toSemilatticeSup	—	Iio_union_Ico LE.le.trans min_le_left
Iio_union_Ico_eq_Iio 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ico	—	Subset.antisymm lt_of_lt_of_le Iio_subset_Iio_union_Ico
Iio_union_Ioi 📖	mathematical	—	Set instUnion Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioi Compl.compl instCompl instSingletonSet	—	ext lt_or_lt_iff_ne
Iio_union_Ioi_of_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioi univ	—	eq_univ_of_forall LT.lt.gt_or_lt
Iio_union_Ioo 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin	Set instUnion Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioo SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Iio_union_Ioo' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioo SemilatticeSup.toMax Lattice.toSemilatticeSup	—	Iio_union_Ioo LE.le.trans_lt min_le_left
Ioc_diff_Iic 📖	mathematical	—	Set instSDiff Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Iic SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Ioc_diff_Ioi 📖	mathematical	—	Set instSDiff Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioi SemilatticeInf.toMin	—	—
Ioc_eq_Ioc_iff 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Ioc_subset_Ioc_iff Eq.subset instReflSubset Eq.superset
Ioc_inter_Ioc 📖	mathematical	—	Set instInter Ioc PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax SemilatticeInf.toMin Lattice.toSemilatticeInf	—	—
Ioc_inter_Ioi 📖	mathematical	—	Set instInter Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioi SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Ioc_inter_Ioo_of_left_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instInter Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioo SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Ioc_inter_Ioo_of_right_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instInter Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioo SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Ioc_subset_Ioc_iff 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instHasSubset Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE	—	Ico_toDual Ico_subset_Ico_iff
Ioc_subset_Ioc_union_Icc 📖	mathematical	—	Set instHasSubset Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instUnion Icc	—	Subset.trans Ioc_subset_Ioc_union_Ioc union_subset_union_right Ioc_subset_Icc_self
Ioc_subset_Ioc_union_Ioc 📖	mathematical	—	Set instHasSubset Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instUnion	—	le_or_gt
Ioc_subset_Ioo_union_Icc 📖	mathematical	—	Set instHasSubset Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instUnion Ioo Icc	—	lt_or_ge
Ioc_union_Icc_eq_Ioc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE	Set instUnion Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Icc	—	Subset.antisymm LE.le.trans LT.lt.trans_le Ioc_subset_Ioc_union_Icc
Ioc_union_Ici_eq_Ioi 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ici Ioi	—	Subset.antisymm LT.lt.trans_le Ioi_subset_Ioc_union_Ici
Ioc_union_Ico_eq_Ioo 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ico Ioo	—	Subset.antisymm LE.le.trans_lt LT.lt.trans_le Ioo_subset_Ioc_union_Ico
Ioc_union_Ioc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	Set instUnion Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Ioc_union_Ioc' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	—	Ioc_union_Ioc LE.le.trans min_le_left le_max_right
Ioc_union_Ioc_eq_Ioc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Subset.antisymm LE.le.trans LE.le.trans_lt Ioc_subset_Ioc_union_Ioc
Ioc_union_Ioc_left 📖	mathematical	—	Set instUnion Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin	—	—
Ioc_union_Ioc_right 📖	mathematical	—	Set instUnion Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Ioc_union_Ioc_symm 📖	mathematical	—	Set instUnion Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Ioc_union_Ioc_union_Ioc_cycle 📖	mathematical	—	Set instUnion Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Ioc_union_Ioi 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup	Set instUnion Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioi SemilatticeInf.toMin	—	—
Ioc_union_Ioi' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioi SemilatticeInf.toMin	—	Ioc_union_Ioi LE.le.trans le_max_right
Ioc_union_Ioi_eq_Ioi 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioi	—	Subset.antisymm LE.le.trans_lt Ioi_subset_Ioc_union_Ioi
Ioc_union_Ioo_eq_Ioo 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	Set instUnion Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioo	—	Subset.antisymm LE.le.trans_lt Ioo_subset_Ioc_union_Ioo
Ioi_diff_Ici 📖	mathematical	—	Set instSDiff Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ici Ioo	—	diff_eq compl_Ici Ioi_inter_Iio
Ioi_diff_Ioc 📖	mathematical	—	Set instSDiff Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioc SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Ioi_diff_Ioi 📖	mathematical	—	Set instSDiff Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioc	—	diff_eq compl_Ioi Ioi_inter_Iic
Ioi_inj 📖	mathematical	—	Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Ioi_injective
Ioi_injective 📖	mathematical	—	Set Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	eq_of_forall_gt_iff ext_iff
Ioi_inter_Ioi 📖	mathematical	—	Set instInter Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup	—	ext sup_lt_iff
Ioi_inter_Ioo 📖	mathematical	—	Set instInter Ioi PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioo SemilatticeSup.toMax	—	—
Ioi_ssubset_Ioi_iff 📖	mathematical	—	Set instHasSSubset Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	—	ssubset_iff_exists LT.lt.trans_le le_of_not_gt Ioi_ssubset_Ioi
Ioi_subset_Ici_iff 📖	mathematical	—	Set instHasSubset Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ici Preorder.toLE	—	exists_between not_le lt_irrefl LT.lt.trans_le Ioi_subset_Ici
Ioi_subset_Ioc_union_Ici 📖	mathematical	—	Set instHasSubset Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instUnion Ioc Ici	—	Subset.trans Ioi_subset_Ioo_union_Ici union_subset_union_left Ioo_subset_Ioc_self
Ioi_subset_Ioc_union_Ioi 📖	mathematical	—	Set instHasSubset Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instUnion Ioc	—	le_or_gt
Ioi_subset_Ioi_iff 📖	mathematical	—	Set instHasSubset Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE	—	lt_irrefl not_le Ioi_subset_Ioi
Ioi_subset_Ioo_union_Ici 📖	mathematical	—	Set instHasSubset Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instUnion Ioo Ici	—	lt_or_ge
Ioi_union_Iic 📖	mathematical	—	Set instUnion Ioi PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Iic univ	—	Ioi_union_Iic_of_le le_rfl
Ioi_union_Iic_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Ioi PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Iic univ	—	eq_univ_of_forall LE.le.le_or_gt
Ioi_union_Iio 📖	mathematical	—	Set instUnion Ioi PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Iio Compl.compl instCompl instSingletonSet	—	ext lt_or_gt_iff_ne'
Ioi_union_Iio_of_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Ioi PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Iio univ	—	eq_univ_of_forall LT.lt.lt_or_gt
Ioo_inter_Iio 📖	mathematical	—	Set instInter Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Iio SemilatticeInf.toMin	—	—
Ioo_inter_Ioc_of_left_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instInter Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioc SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Ioo_inter_Ioc_of_right_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instInter Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioc SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Ioo_inter_Ioi 📖	mathematical	—	Set instInter Ioo PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioi SemilatticeSup.toMax	—	—
Ioo_inter_Ioo 📖	mathematical	—	Set instInter Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup SemilatticeInf.toMin	—	—
Ioo_subset_Ioc_union_Ico 📖	mathematical	—	Set instHasSubset Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instUnion Ioc Ico	—	Subset.trans Ioo_subset_Ioc_union_Ioo union_subset_union_right Ioo_subset_Ico_self
Ioo_subset_Ioc_union_Ioo 📖	mathematical	—	Set instHasSubset Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instUnion Ioc	—	le_or_gt
Ioo_subset_Ioo_iff 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instHasSubset Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE	—	exists_between le_of_not_gt LT.lt.trans lt_irrefl Ioo_subset_Ioo
Ioo_subset_Ioo_union_Ico 📖	mathematical	—	Set instHasSubset Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instUnion Ico	—	lt_or_ge
Ioo_subset_Ioo_union_Ioo 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	Set instHasSubset Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instUnion	—	lt_or_ge lt_of_le_of_lt lt_of_lt_of_le
Ioo_union_Icc_eq_Ioc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE	Set instUnion Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Icc Ioc	—	Subset.antisymm LE.le.trans LT.lt.le LT.lt.trans_le Ioc_subset_Ioo_union_Icc
Ioo_union_Ici_eq_Ioi 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ici Ioi	—	Subset.antisymm LT.lt.trans_le Ioi_subset_Ioo_union_Ici
Ioo_union_Ico_eq_Ioo 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE	Set instUnion Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ico	—	Subset.antisymm LT.lt.trans_le Ioo_subset_Ioo_union_Ico
Ioo_union_Ioi 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup	Set instUnion Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioi SemilatticeInf.toMin	—	—
Ioo_union_Ioi' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioi SemilatticeInf.toMin	—	Ioo_union_Ioi LT.lt.trans_le le_max_right
Ioo_union_Ioo 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	Set instUnion Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Ioo_union_Ioo' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
compl_Ici 📖	mathematical	—	Compl.compl Set instCompl Ici PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Iio	—	ext not_le
compl_Iic 📖	mathematical	—	Compl.compl Set instCompl Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioi	—	ext not_le
compl_Iio 📖	mathematical	—	Compl.compl Set instCompl Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ici	—	ext not_lt
compl_Ioc 📖	mathematical	—	Compl.compl Set instCompl Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instUnion Iic Ioi	—	—
compl_Ioi 📖	mathematical	—	Compl.compl Set instCompl Ioi PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Iic	—	ext not_lt
notMem_Ici 📖	mathematical	—	Set instMembership Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	—	not_le
notMem_Iic 📖	mathematical	—	Set instMembership Iic PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	—	not_le
notMem_Iio 📖	mathematical	—	Set instMembership Iio PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE	—	not_lt
notMem_Ioi 📖	mathematical	—	Set instMembership Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE	—	not_lt

(root)

Definitions

Name	Category	Theorems
LinearOrder 📖	CompData	21 math math: MonovaryOn.exists_monotoneOn, Antivary.exists_antitone_monotone, AntivaryOn.exists_antitoneOn_monotoneOn, exists_wellOrder, monovaryOn_iff_exists_monotoneOn, antivaryOn_iff_exists_monotoneOn_antitoneOn, antivary_iff_exists_monotone_antitone, monovary_iff_exists_antitone, LinearOrder.toPartialOrder_injective, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_transfiniteCompositionOfShape, Monovary.exists_monotone, AntivaryOn.exists_monotoneOn_antitoneOn, MonovaryOn.exists_antitoneOn, antivaryOn_iff_exists_antitoneOn_monotoneOn, CategoryTheory.MorphismProperty.transfiniteCompositions_iff, Cardinal.exists_ord_eq_type_lt, monovaryOn_iff_exists_antitoneOn, Antivary.exists_monotone_antitone, antivary_iff_exists_antitone_monotone, monovary_iff_exists_monotone, Monovary.exists_antitone

---

← Back to Index