ModularLattice

📁 Source: Mathlib/Order/ModularLattice.lean

Statistics

Metric	Count
Definitions IicOrderIsoIci, IsLowerModularLattice, IsModularLattice, IsUpperModularLattice, IsWeakLowerModularLattice, IsWeakUpperModularLattice, infIccOrderIsoIccSup, infIooOrderIsoIooSup	8
Theorems codisjoint_inf_left_of_codisjoint_inf_right, codisjoint_inf_right_of_codisjoint_inf_left, exists_isCompl, isCompl_inf_left_of_isCompl_inf_right, isCompl_inf_right_of_isCompl_inf_left, inf_of_sup_left, inf_of_sup_of_sup_left, inf_of_sup_of_sup_right, inf_of_sup_right, sup_of_inf_left, sup_of_inf_of_inf_left, sup_of_inf_of_inf_right, sup_of_inf_right, disjoint_sup_left_of_disjoint_sup_right, disjoint_sup_right_of_disjoint_sup_left, exists_isCompl, isCompl_sup_left_of_isCompl_sup_right, isCompl_sup_right_of_isCompl_sup_left, instIsModularLattice, inf_covBy_of_covBy_sup, to_isWeakLowerModularLattice, complementedLattice_Icc, complementedLattice_Ici, complementedLattice_Iic, exists_disjoint_and_sup_eq, exists_inf_eq_and_codisjoint, exists_inf_eq_and_sup_eq, inf_sup_inf_assoc, isModularLattice_Ici, isModularLattice_Iic, sup_inf_le_assoc_of_le, sup_inf_sup_assoc, to_isLowerModularLattice, to_isUpperModularLattice, covBy_sup_of_inf_covBy, to_isWeakUpperModularLattice, inf_covBy_of_covBy_covBy_sup, covBy_sup_of_inf_covBy_covBy, isCompl_inf_inf_of_isCompl_of_le, codisjoint_inf_right_of_codisjoint_inf_right, covBy_sup_of_inf_covBy_left, covBy_sup_of_inf_covBy_of_inf_covBy_left, covBy_sup_of_inf_covBy_of_inf_covBy_right, covBy_sup_of_inf_covBy_right, disjoint_sup_right_of_disjoint_sup_right, eq_of_le_of_inf_le_of_le_sup, eq_of_le_of_inf_le_of_sup_le, eq_of_le_of_sup_le_of_inf_le, eq_of_le_of_sup_le_of_le_inf, infIccOrderIsoIccSup_apply_coe, infIccOrderIsoIccSup_symm_apply_coe, infIooOrderIsoIooSup_apply_coe, infIooOrderIsoIooSup_symm_apply_coe, inf_covBy_of_covBy_sup_left, inf_covBy_of_covBy_sup_of_covBy_sup_left, inf_covBy_of_covBy_sup_of_covBy_sup_right, inf_covBy_of_covBy_sup_right, inf_lt_inf_of_lt_of_sup_le_sup, inf_strictMonoOn_Icc_sup, inf_sup_assoc_of_le, inf_sup_le_assoc_of_le, instIsLowerModularLatticeOrderDual, instIsModularLatticeOrderDual, instIsUpperModularLatticeOrderDual, instIsWeakLowerModularLatticeOrderDual, instIsWeakUpperModularLatticeOrderDual, isModularLattice_iff_inf_sup_inf_assoc, le_iff_eq_of_codisjoint_of_disjoint, strictMono_inf_prod_sup, sup_inf_assoc_of_le, sup_inf_le_assoc_of_le, sup_lt_sup_of_lt_of_inf_le_inf, sup_strictMonoOn_Icc_inf, wellFounded_gt_exact_sequence, wellFounded_lt_exact_sequence	75
Total	83

Codisjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
codisjoint_inf_left_of_codisjoint_inf_right 📖	mathematical	Codisjoint SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup SemilatticeInf.toMin Lattice.toSemilatticeInf	Codisjoint SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup SemilatticeInf.toMin Lattice.toSemilatticeInf	—	codisjoint_comm inf_comm codisjoint_inf_right_of_codisjoint_inf_left symm
codisjoint_inf_right_of_codisjoint_inf_left 📖	mathematical	Codisjoint SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup SemilatticeInf.toMin Lattice.toSemilatticeInf	Codisjoint SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup SemilatticeInf.toMin Lattice.toSemilatticeInf	—	codisjoint_iff_le_sup eq_top inf_comm sup_le le_sup_left LE.le.trans' sup_le_sup_right inf_le_right IsModularLattice.inf_sup_inf_assoc top_inf_eq le_refl
exists_isCompl 📖	mathematical	Codisjoint SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup BoundedOrder.toOrderTop Preorder.toLE PartialOrder.toPreorder	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup IsCompl	—	ComplementedLattice.exists_isCompl inf_le_right isCompl_inf_left_of_isCompl_inf_right IsCompl.symm
isCompl_inf_left_of_isCompl_inf_right 📖	mathematical	Codisjoint SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup BoundedOrder.toOrderTop Preorder.toLE PartialOrder.toPreorder IsCompl SemilatticeInf.toMin Lattice.toSemilatticeInf	IsCompl SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup SemilatticeInf.toMin Lattice.toSemilatticeInf	—	disjoint_assoc IsCompl.disjoint codisjoint_inf_left_of_codisjoint_inf_right IsCompl.codisjoint
isCompl_inf_right_of_isCompl_inf_left 📖	mathematical	Codisjoint SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup BoundedOrder.toOrderTop Preorder.toLE PartialOrder.toPreorder IsCompl SemilatticeInf.toMin Lattice.toSemilatticeInf	IsCompl SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup SemilatticeInf.toMin Lattice.toSemilatticeInf	—	disjoint_assoc IsCompl.disjoint codisjoint_inf_right_of_codisjoint_inf_left IsCompl.codisjoint

CovBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inf_of_sup_left 📖	mathematical	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup SemilatticeSup.toMax	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup SemilatticeInf.toMin Lattice.toSemilatticeInf	—	inf_covBy_of_covBy_sup_left
inf_of_sup_of_sup_left 📖	mathematical	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup SemilatticeSup.toMax	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup SemilatticeInf.toMin Lattice.toSemilatticeInf	—	inf_covBy_of_covBy_sup_of_covBy_sup_left
inf_of_sup_of_sup_right 📖	mathematical	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup SemilatticeSup.toMax	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup SemilatticeInf.toMin Lattice.toSemilatticeInf	—	inf_covBy_of_covBy_sup_of_covBy_sup_right
inf_of_sup_right 📖	mathematical	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup SemilatticeSup.toMax	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup SemilatticeInf.toMin Lattice.toSemilatticeInf	—	inf_covBy_of_covBy_sup_right
sup_of_inf_left 📖	mathematical	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeInf.toMin	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeSup.toMax Lattice.toSemilatticeSup	—	covBy_sup_of_inf_covBy_left
sup_of_inf_of_inf_left 📖	mathematical	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeInf.toMin	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeSup.toMax Lattice.toSemilatticeSup	—	covBy_sup_of_inf_covBy_of_inf_covBy_left
sup_of_inf_of_inf_right 📖	mathematical	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeInf.toMin	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeSup.toMax Lattice.toSemilatticeSup	—	covBy_sup_of_inf_covBy_of_inf_covBy_right
sup_of_inf_right 📖	mathematical	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeInf.toMin	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeSup.toMax Lattice.toSemilatticeSup	—	covBy_sup_of_inf_covBy_right

Disjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
disjoint_sup_left_of_disjoint_sup_right 📖	mathematical	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeSup.toMax Lattice.toSemilatticeSup	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeSup.toMax Lattice.toSemilatticeSup	—	disjoint_comm sup_comm disjoint_sup_right_of_disjoint_sup_left symm
disjoint_sup_right_of_disjoint_sup_left 📖	mathematical	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeSup.toMax Lattice.toSemilatticeSup	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeSup.toMax Lattice.toSemilatticeSup	—	disjoint_iff_inf_le eq_bot sup_comm le_inf inf_le_left LE.le.trans inf_le_inf_right le_sup_right IsModularLattice.sup_inf_sup_assoc bot_sup_eq le_refl
exists_isCompl 📖	mathematical	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf IsCompl	—	ComplementedLattice.exists_isCompl le_sup_right isCompl_sup_left_of_isCompl_sup_right IsCompl.symm
isCompl_sup_left_of_isCompl_sup_right 📖	mathematical	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder IsCompl SemilatticeSup.toMax Lattice.toSemilatticeSup	IsCompl SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeSup.toMax Lattice.toSemilatticeSup	—	disjoint_sup_left_of_disjoint_sup_right IsCompl.disjoint codisjoint_assoc IsCompl.codisjoint
isCompl_sup_right_of_isCompl_sup_left 📖	mathematical	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder IsCompl SemilatticeSup.toMax Lattice.toSemilatticeSup	IsCompl SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeSup.toMax Lattice.toSemilatticeSup	—	disjoint_sup_right_of_disjoint_sup_left IsCompl.disjoint codisjoint_assoc IsCompl.codisjoint

DistribLattice

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsModularLattice 📖	mathematical	—	IsModularLattice toLattice	—	inf_sup_right inf_eq_left le_refl

IsCompl

Definitions

Name	Category	Theorems
IicOrderIsoIci 📖	CompOp	—

IsLowerModularLattice

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inf_covBy_of_covBy_sup 📖	mathematical	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeSup.toMax Lattice.toSemilatticeSup	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeInf.toMin	—	—
to_isWeakLowerModularLattice 📖	mathematical	—	IsWeakLowerModularLattice	—	CovBy.inf_of_sup_right

IsModularLattice

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
complementedLattice_Icc 📖	mathematical	—	ComplementedLattice Set.Elem Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf Set.Icc.lattice Set.Icc.instBoundedOrderElemOfFactLe	—	exists_inf_eq_and_sup_eq inf_le_right le_sup_right
complementedLattice_Ici 📖	mathematical	—	ComplementedLattice Set.Elem Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf Set.Ici.lattice Set.Ici.boundedOrder BoundedOrder.toOrderTop Preorder.toLE	—	exists_inf_eq_and_codisjoint inf_le_right
complementedLattice_Iic 📖	mathematical	—	ComplementedLattice Set.Elem Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf Set.Iic.instLatticeElem Set.Iic.instBoundedOrderElemOfOrderBot BoundedOrder.toOrderBot Preorder.toLE	—	exists_disjoint_and_sup_eq le_sup_right
exists_disjoint_and_sup_eq 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toMax Lattice.toSemilatticeSup	—	exists_inf_eq_and_sup_eq
exists_inf_eq_and_codisjoint 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf	SemilatticeInf.toMin Lattice.toSemilatticeInf Codisjoint SemilatticeInf.toPartialOrder BoundedOrder.toOrderTop Preorder.toLE PartialOrder.toPreorder	—	exists_inf_eq_and_sup_eq
exists_inf_eq_and_sup_eq 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf	SemilatticeInf.toMin Lattice.toSemilatticeInf SemilatticeSup.toMax Lattice.toSemilatticeSup	—	ComplementedLattice.exists_isCompl inf_sup_assoc_of_le Disjoint.eq_bot sup_of_le_right LE.le.trans sup_inf_assoc_of_le Codisjoint.eq_top sup_of_le_left inf_of_le_right
inf_sup_inf_assoc 📖	mathematical	—	SemilatticeSup.toMax Lattice.toSemilatticeSup SemilatticeInf.toMin Lattice.toSemilatticeInf	—	sup_inf_assoc_of_le inf_le_right
isModularLattice_Ici 📖	mathematical	—	IsModularLattice Set.Elem Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf Set.Ici.lattice	—	sup_inf_le_assoc_of_le
isModularLattice_Iic 📖	mathematical	—	IsModularLattice Set.Elem Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf Set.Iic.instLatticeElem	—	sup_inf_le_assoc_of_le
sup_inf_le_assoc_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
sup_inf_sup_assoc 📖	mathematical	—	SemilatticeInf.toMin Lattice.toSemilatticeInf SemilatticeSup.toMax Lattice.toSemilatticeSup	—	inf_sup_assoc_of_le le_sup_right
to_isLowerModularLattice 📖	mathematical	—	IsLowerModularLattice	—	sup_comm inf_comm Equiv.isEmpty_congr
to_isUpperModularLattice 📖	mathematical	—	IsUpperModularLattice	—	Equiv.isEmpty_congr

IsUpperModularLattice

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
covBy_sup_of_inf_covBy 📖	mathematical	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeInf.toMin	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
to_isWeakUpperModularLattice 📖	mathematical	—	IsWeakUpperModularLattice	—	CovBy.sup_of_inf_right

IsWeakLowerModularLattice

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inf_covBy_of_covBy_covBy_sup 📖	mathematical	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeSup.toMax Lattice.toSemilatticeSup	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeInf.toMin	—	—

IsWeakUpperModularLattice

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
covBy_sup_of_inf_covBy_covBy 📖	mathematical	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeInf.toMin	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—

Set.Iic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCompl_inf_inf_of_isCompl_of_le 📖	mathematical	IsCompl SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf Preorder.toLE PartialOrder.toPreorder	IsCompl Set Set.instMembership Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf Subtype.partialOrder instBoundedOrderElemOfOrderBot BoundedOrder.toOrderBot Preorder.toLE SemilatticeInf.toMin inf_le_left	—	inf_le_left inf_comm inf_assoc IsCompl.inf_eq_bot inf_of_le_left inf_of_le_right IsModularLattice.inf_sup_inf_assoc IsCompl.sup_eq_top

(root)

Definitions

Name	Category	Theorems
IsLowerModularLattice 📖	CompData	2 math math: instIsLowerModularLatticeOrderDual, IsModularLattice.to_isLowerModularLattice
IsModularLattice 📖	CompData	9 math math: instIsModularLatticeOrderDual, instIsModularLatticeSubgroup, instIsModularLatticeAddSubgroup, DistribLattice.instIsModularLattice, IsModularLattice.isModularLattice_Ici, IsModularLattice.isModularLattice_Iic, Submodule.instIsModularLattice, isModularLattice_iff_inf_sup_inf_assoc, LieSubmodule.instIsModularLattice
IsUpperModularLattice 📖	CompData	2 math math: instIsUpperModularLatticeOrderDual, IsModularLattice.to_isUpperModularLattice
IsWeakLowerModularLattice 📖	CompData	2 math math: instIsWeakLowerModularLatticeOrderDual, IsLowerModularLattice.to_isWeakLowerModularLattice
IsWeakUpperModularLattice 📖	CompData	2 math math: IsUpperModularLattice.to_isWeakUpperModularLattice, instIsWeakUpperModularLatticeOrderDual
infIccOrderIsoIccSup 📖	CompOp	2 math math: infIccOrderIsoIccSup_apply_coe, infIccOrderIsoIccSup_symm_apply_coe
infIooOrderIsoIooSup 📖	CompOp	2 math math: infIooOrderIsoIooSup_symm_apply_coe, infIooOrderIsoIooSup_apply_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
codisjoint_inf_right_of_codisjoint_inf_right 📖	mathematical	Codisjoint SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup SemilatticeInf.toMin Lattice.toSemilatticeInf	Codisjoint SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup SemilatticeInf.toMin Lattice.toSemilatticeInf	—	inf_comm codisjoint_comm Codisjoint.codisjoint_inf_left_of_codisjoint_inf_right Codisjoint.mono_right inf_le_right
covBy_sup_of_inf_covBy_left 📖	mathematical	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeInf.toMin	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeSup.toMax Lattice.toSemilatticeSup	—	IsUpperModularLattice.covBy_sup_of_inf_covBy
covBy_sup_of_inf_covBy_of_inf_covBy_left 📖	mathematical	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeInf.toMin	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeSup.toMax Lattice.toSemilatticeSup	—	IsWeakUpperModularLattice.covBy_sup_of_inf_covBy_covBy
covBy_sup_of_inf_covBy_of_inf_covBy_right 📖	mathematical	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeInf.toMin	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeSup.toMax Lattice.toSemilatticeSup	—	inf_comm sup_comm covBy_sup_of_inf_covBy_of_inf_covBy_left
covBy_sup_of_inf_covBy_right 📖	mathematical	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeInf.toMin	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeSup.toMax Lattice.toSemilatticeSup	—	sup_comm inf_comm covBy_sup_of_inf_covBy_left
disjoint_sup_right_of_disjoint_sup_right 📖	mathematical	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeSup.toMax Lattice.toSemilatticeSup	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeSup.toMax Lattice.toSemilatticeSup	—	sup_comm disjoint_comm Disjoint.disjoint_sup_left_of_disjoint_sup_right Disjoint.mono_right le_sup_right
eq_of_le_of_inf_le_of_le_sup 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—	LE.le.antisymm sup_inf_assoc_of_le inf_eq_right sup_le_iff Eq.le inf_comm
eq_of_le_of_inf_le_of_sup_le 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—	eq_of_le_of_inf_le_of_le_sup LE.le.trans inf_le_left le_sup_left
eq_of_le_of_sup_le_of_inf_le 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup SemilatticeSup.toMax SemilatticeInf.toMin Lattice.toSemilatticeInf	—	—	eq_of_le_of_sup_le_of_le_inf LE.le.trans' le_sup_left inf_le_left
eq_of_le_of_sup_le_of_le_inf 📖	—	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup SemilatticeSup.toMax SemilatticeInf.toMin Lattice.toSemilatticeInf	—	—	LE.le.antisymm' inf_sup_assoc_of_le sup_eq_right le_inf_iff Eq.ge sup_comm
infIccOrderIsoIccSup_apply_coe 📖	mathematical	—	Set Set.instMembership Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeSup.toMax Lattice.toSemilatticeSup DFunLike.coe RelIso Set.Elem SemilatticeInf.toMin Preorder.toLE RelIso.instFunLike infIccOrderIsoIccSup	—	—
infIccOrderIsoIccSup_symm_apply_coe 📖	mathematical	—	Set Set.instMembership Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeInf.toMin DFunLike.coe RelIso Set.Elem SemilatticeSup.toMax Lattice.toSemilatticeSup Preorder.toLE RelIso.instFunLike RelIso.symm infIccOrderIsoIccSup	—	—
infIooOrderIsoIooSup_apply_coe 📖	mathematical	—	Set Set.instMembership Set.Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeSup.toMax Lattice.toSemilatticeSup DFunLike.coe RelIso Set.Elem SemilatticeInf.toMin Preorder.toLE RelIso.instFunLike infIooOrderIsoIooSup	—	—
infIooOrderIsoIooSup_symm_apply_coe 📖	mathematical	—	Set Set.instMembership Set.Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeInf.toMin DFunLike.coe RelIso Set.Elem SemilatticeSup.toMax Lattice.toSemilatticeSup Preorder.toLE RelIso.instFunLike RelIso.symm infIooOrderIsoIooSup	—	—
inf_covBy_of_covBy_sup_left 📖	mathematical	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup SemilatticeSup.toMax	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup SemilatticeInf.toMin Lattice.toSemilatticeInf	—	IsLowerModularLattice.inf_covBy_of_covBy_sup
inf_covBy_of_covBy_sup_of_covBy_sup_left 📖	mathematical	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup SemilatticeSup.toMax	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup SemilatticeInf.toMin Lattice.toSemilatticeInf	—	IsWeakLowerModularLattice.inf_covBy_of_covBy_covBy_sup
inf_covBy_of_covBy_sup_of_covBy_sup_right 📖	mathematical	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup SemilatticeSup.toMax	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup SemilatticeInf.toMin Lattice.toSemilatticeInf	—	sup_comm inf_comm inf_covBy_of_covBy_sup_of_covBy_sup_left
inf_covBy_of_covBy_sup_right 📖	mathematical	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup SemilatticeSup.toMax	CovBy Preorder.toLT PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup SemilatticeInf.toMin Lattice.toSemilatticeInf	—	inf_comm sup_comm inf_covBy_of_covBy_sup_left
inf_lt_inf_of_lt_of_sup_le_sup 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup Preorder.toLE SemilatticeSup.toMax	Preorder.toLT PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup SemilatticeInf.toMin Lattice.toSemilatticeInf	—	lt_of_le_of_ne' inf_le_inf_right le_of_lt ne_of_gt eq_of_le_of_sup_le_of_inf_le ge_of_eq
inf_strictMonoOn_Icc_sup 📖	mathematical	—	StrictMonoOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeInf.toMin Set.Icc SemilatticeSup.toMax Lattice.toSemilatticeSup	—	StrictMono.of_restrict OrderIso.strictMono
inf_sup_assoc_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup	SemilatticeSup.toMax Lattice.toSemilatticeSup SemilatticeInf.toMin Lattice.toSemilatticeInf	—	ge_antisymm inf_sup_le_assoc_of_le sup_le inf_le_inf_left le_sup_left le_inf le_sup_right
inf_sup_le_assoc_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	—	inf_comm sup_comm sup_inf_le_assoc_of_le
instIsLowerModularLatticeOrderDual 📖	mathematical	—	IsLowerModularLattice OrderDual OrderDual.instLattice	—	CovBy.toDual CovBy.sup_of_inf_left CovBy.ofDual
instIsModularLatticeOrderDual 📖	mathematical	—	IsModularLattice OrderDual OrderDual.instLattice	—	le_of_eq inf_comm sup_comm sup_inf_assoc_of_le
instIsUpperModularLatticeOrderDual 📖	mathematical	—	IsUpperModularLattice OrderDual OrderDual.instLattice	—	CovBy.toDual CovBy.inf_of_sup_left CovBy.ofDual
instIsWeakLowerModularLatticeOrderDual 📖	mathematical	—	IsWeakLowerModularLattice OrderDual OrderDual.instLattice	—	CovBy.toDual CovBy.sup_of_inf_of_inf_left CovBy.ofDual
instIsWeakUpperModularLatticeOrderDual 📖	mathematical	—	IsWeakUpperModularLattice OrderDual OrderDual.instLattice	—	CovBy.toDual CovBy.inf_of_sup_of_sup_left CovBy.ofDual
isModularLattice_iff_inf_sup_inf_assoc 📖	mathematical	—	IsModularLattice SemilatticeSup.toMax Lattice.toSemilatticeSup SemilatticeInf.toMin Lattice.toSemilatticeInf	—	IsModularLattice.inf_sup_inf_assoc inf_eq_left le_refl
le_iff_eq_of_codisjoint_of_disjoint 📖	mathematical	Codisjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf BoundedOrder.toOrderTop Preorder.toLE PartialOrder.toPreorder Disjoint BoundedOrder.toOrderBot	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf	—	le_antisymm Codisjoint.eq_top inf_of_le_right Disjoint.eq_bot sup_of_le_left sup_inf_le_assoc_of_le le_of_eq
strictMono_inf_prod_sup 📖	mathematical	—	StrictMono PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf Prod.instPreorder SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	—	inf_le_inf_right LT.lt.le sup_le_sup_right LT.lt.not_ge sup_lt_sup_of_lt_of_inf_le_inf
sup_inf_assoc_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf	SemilatticeInf.toMin Lattice.toSemilatticeInf SemilatticeSup.toMax Lattice.toSemilatticeSup	—	le_antisymm sup_inf_le_assoc_of_le le_inf sup_le_sup_left inf_le_left sup_le inf_le_right
sup_inf_le_assoc_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	—	IsModularLattice.sup_inf_le_assoc_of_le
sup_lt_sup_of_lt_of_inf_le_inf 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf Preorder.toLE SemilatticeInf.toMin	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeSup.toMax Lattice.toSemilatticeSup	—	lt_of_le_of_ne sup_le_sup_right le_of_lt ne_of_lt eq_of_le_of_inf_le_of_sup_le le_of_eq
sup_strictMonoOn_Icc_inf 📖	mathematical	—	StrictMonoOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf SemilatticeSup.toMax Lattice.toSemilatticeSup Set.Icc SemilatticeInf.toMin	—	StrictMono.of_restrict OrderIso.strictMono
wellFounded_gt_exact_sequence 📖	mathematical	SemilatticeInf.toMin Lattice.toSemilatticeInf SemilatticeSup.toMax Lattice.toSemilatticeSup	WellFoundedGT Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf	—	wellFounded_lt_exact_sequence instIsModularLatticeOrderDual instWellFoundedLTOrderDualOfWellFoundedGT
wellFounded_lt_exact_sequence 📖	mathematical	SemilatticeInf.toMin Lattice.toSemilatticeInf SemilatticeSup.toMax Lattice.toSemilatticeSup	WellFoundedLT Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf	—	StrictMono.wellFoundedLT Prod.wellFoundedLT GaloisCoinsertion.l_le_l_iff GaloisInsertion.u_le_u_iff strictMono_inf_prod_sup

---

← Back to Index