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, 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_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_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, 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	138
Total	139

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	—	—
Icc_union_Icc' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Icc 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	—	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 Ici SemilatticeInf.toMin	—	—
Icc_union_Ici' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Icc Ici SemilatticeInf.toMin	—	—
Icc_union_Ici_eq_Ici 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Icc 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 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 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 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 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
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	—	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 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 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 Ici SemilatticeInf.toMin	—	—
Ico_union_Ici' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Ico Ici SemilatticeInf.toMin	—	—
Ico_union_Ici_eq_Ici 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Ico 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	—	—
Ico_union_Ico' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Ico SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Ico_union_Ico_eq_Ico 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Ico	—	Subset.antisymm LT.lt.trans_le LE.le.trans Ico_subset_Ico_union_Ico
Iic_diff_Iic 📖	mathematical	—	Set instSDiff Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioc	—	diff_eq compl_Iic inter_comm Ioi_inter_Iic
Iic_diff_Iio 📖	mathematical	—	Set instSDiff Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Iio Icc	—	diff_eq compl_Iio inter_comm Ici_inter_Iic
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 Ioc	—	—
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 Icc SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Iic_union_Icc' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Iic Icc SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Iic_union_Icc_eq_Iic 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Iic 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 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 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 Ioc SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Iic_union_Ioc' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Iic Ioc SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Iic_union_Ioc_eq_Iic 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Iic 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 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 Ioo Iio	—	Subset.antisymm lt_of_le_of_lt Iio_subset_Iic_union_Ioo
Iio_diff_Iic 📖	mathematical	—	Set instSDiff Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Iic Ioo	—	diff_eq compl_Iic inter_comm Ioi_inter_Iio
Iio_diff_Iio 📖	mathematical	—	Set instSDiff Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ico	—	diff_eq compl_Iio inter_comm Ici_inter_Iio
Iio_inj 📖	mathematical	—	Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Iio_injective
Iio_injective 📖	mathematical	—	Set Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	eq_of_forall_lt_iff ext_iff
Iio_inter_Iio 📖	mathematical	—	Set instInter Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin	—	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 SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	—	ssubset_iff_exists LE.le.trans_lt le_of_not_gt Iio_ssubset_Iio
Iio_subset_Iic_iff 📖	mathematical	—	Set instHasSubset Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Iic Preorder.toLE	—	diff_eq_empty Iio_diff_Iic Ioo_eq_empty_iff not_lt
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 SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf 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 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 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 Ico SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Iio_union_Ico' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Iio Ico SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Iio_union_Ico_eq_Iio 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Iio 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 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 Ioo SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Iio_union_Ioo' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Iio Ioo SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
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	—	Ioc_subset_Ioc_iff Eq.subset instReflSubset Eq.superset
Ioc_inter_Ioc 📖	mathematical	—	Set instInter Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeSup.toMax Lattice.toSemilatticeSup SemilatticeInf.toMin	—	—
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 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 Ioo SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Ioc_subset_Ioc_iff 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instHasSubset Ioc 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 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 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 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	—	—
Ioc_union_Ioc' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Ioc SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Ioc_union_Ioc_eq_Ioc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Ioc	—	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 Ioi SemilatticeInf.toMin	—	—
Ioc_union_Ioi' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Ioc Ioi SemilatticeInf.toMin	—	—
Ioc_union_Ioi_eq_Ioi 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Ioc 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 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_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 SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioo SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
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
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 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 Ioc SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
Ioo_inter_Ioi 📖	mathematical	—	Set instInter Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Ioi SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
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 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 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 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 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 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 Ioi SemilatticeInf.toMin	—	—
Ioo_union_Ioi' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Ioo Ioi SemilatticeInf.toMin	—	—
Ioo_union_Ioo 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	Set instUnion Ioo	—	—
Ioo_union_Ioo' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set instUnion Ioo SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
compl_Ici 📖	mathematical	—	Compl.compl Set instCompl Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf 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 SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf 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 SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT	—	not_le
notMem_Iio 📖	mathematical	—	Set instMembership Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf 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	1 math math: LinearOrder.toPartialOrder_injective

---

← Back to Index