Completion

📁 Source: Mathlib/Order/Completion.lean

Statistics

Metric	Count
Definitions `DedekindCut`, `factorEmbedding`, `instCompleteLinearOrder`, `instDecidableLE`, `instLinearOrder`, `left`, `principal`, `principalEmbedding`, `principalIso`, `right`	10
Theorems `coe_principalEmbedding`, `ext`, `ext'`, `ext_iff`, `factorEmbedding_apply`, `factorEmbedding_principal`, `image_left_subset_lowerBounds`, `image_right_subset_upperBounds`, `instTotalLe`, `left_principal`, `lowerBounds_right`, `ofAttribute_eq_principal`, `ofObject_eq_principal`, `principalEmbedding_apply`, `principalEmbedding_trans_factorEmbedding`, `principalIso_apply`, `principalIso_symm_apply`, `principal_inj`, `principal_le_principal`, `principal_lt_principal`, `principal_sInf_right`, `principal_sSup_left`, `right_principal`, `upperBounds_left`	24
Total	34

DedekindCut

Definitions

Name	Category	Theorems
`factorEmbedding` 📖	CompOp	3 math math: `principalEmbedding_trans_factorEmbedding`, `factorEmbedding_apply`, `factorEmbedding_principal`
`instCompleteLinearOrder` 📖	CompOp	—
`instDecidableLE` 📖	CompOp	—
`instLinearOrder` 📖	CompOp	—
`left` 📖	CompOp	9 math math: `factorEmbedding_apply`, `left_principal`, `principal_sSup_left`, `upperBounds_left`, `ext_iff`, `image_left_subset_lowerBounds`, `lowerBounds_right`, `image_right_subset_upperBounds`, `principalIso_symm_apply`
`principal` 📖	CompOp	13 math math: `principalEmbedding_apply`, `coe_principalEmbedding`, `left_principal`, `principal_sSup_left`, `principal_lt_principal`, `principal_le_principal`, `right_principal`, `factorEmbedding_principal`, `ofAttribute_eq_principal`, `principal_sInf_right`, `principalIso_apply`, `ofObject_eq_principal`, `principal_inj`
`principalEmbedding` 📖	CompOp	3 math math: `principalEmbedding_apply`, `principalEmbedding_trans_factorEmbedding`, `coe_principalEmbedding`
`principalIso` 📖	CompOp	2 math math: `principalIso_apply`, `principalIso_symm_apply`
`right` 📖	CompOp	6 math math: `upperBounds_left`, `right_principal`, `principal_sInf_right`, `image_left_subset_lowerBounds`, `lowerBounds_right`, `image_right_subset_upperBounds`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_principalEmbedding` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `DedekindCut` `PartialOrder.toPreorder` `Preorder.toLE` `Concept.instPartialOrder` `instFunLikeOrderEmbedding` `principalEmbedding` `principal`	—	—
`ext` 📖	—	`left`	—	—	`Concept.ext`
`ext'` 📖	—	`right`	—	—	`Concept.ext'`
`ext_iff` 📖	mathematical	—	`left`	—	`ext`
`factorEmbedding_apply` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `DedekindCut` `PartialOrder.toPreorder` `Preorder.toLE` `Concept.instPartialOrder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `instFunLikeOrderEmbedding` `factorEmbedding` `SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `Set.image` `left`	—	—
`factorEmbedding_principal` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `DedekindCut` `PartialOrder.toPreorder` `Preorder.toLE` `Concept.instPartialOrder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `instFunLikeOrderEmbedding` `factorEmbedding` `principal`	—	`factorEmbedding_apply` `le_antisymm` `le_sSup_iff` `RelEmbedding.instEmbeddingLike` `instReflLe`
`image_left_subset_lowerBounds` 📖	mathematical	`Monotone`	`Set` `Set.instHasSubset` `Set.image` `left` `lowerBounds` `Preorder.toLE` `right`	—	`Concept.rel_extent_intent`
`image_right_subset_upperBounds` 📖	mathematical	`Monotone`	`Set` `Set.instHasSubset` `Set.image` `right` `upperBounds` `Preorder.toLE` `left`	—	`Concept.rel_extent_intent`
`instTotalLe` 📖	mathematical	—	`DedekindCut` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE` `Concept.instPartialOrder`	—	`le_total` `Concept.isLowerSet_extent_le`
`left_principal` 📖	mathematical	—	`left` `principal` `Set.Iic`	—	—
`lowerBounds_right` 📖	mathematical	—	`lowerBounds` `Preorder.toLE` `right` `left`	—	`Concept.lowerPolar_intent`
`ofAttribute_eq_principal` 📖	mathematical	—	`Concept.ofAttribute` `Preorder.toLE` `principal`	—	`ext` `Set.ext` `lowerBounds_singleton`
`ofObject_eq_principal` 📖	mathematical	—	`Concept.ofObject` `Preorder.toLE` `principal`	—	`Concept.copy_eq`
`principalEmbedding_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `DedekindCut` `PartialOrder.toPreorder` `Preorder.toLE` `Concept.instPartialOrder` `RelEmbedding.instFunLike` `principalEmbedding` `principal`	—	—
`principalEmbedding_trans_factorEmbedding` 📖	mathematical	—	`RelEmbedding.trans` `DedekindCut` `PartialOrder.toPreorder` `Preorder.toLE` `Concept.instPartialOrder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `principalEmbedding` `factorEmbedding`	—	`RelEmbedding.ext` `factorEmbedding_principal`
`principalIso_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `DedekindCut` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `Preorder.toLE` `Concept.instPartialOrder` `RelIso.instFunLike` `principalIso` `principal`	—	—
`principalIso_symm_apply` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `DedekindCut` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `Preorder.toLE` `Concept.instPartialOrder` `instFunLikeOrderIso` `OrderIso.symm` `principalIso` `SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `left`	—	`factorEmbedding_apply` `Set.image_congr` `Set.image_id'`
`principal_inj` 📖	mathematical	—	`principal` `PartialOrder.toPreorder`	—	—
`principal_le_principal` 📖	mathematical	—	`DedekindCut` `Preorder.toLE` `PartialOrder.toPreorder` `Concept.instPartialOrder` `principal`	—	`ofObject_eq_principal` `ofAttribute_eq_principal` `Concept.ofObject_le_ofAttribute_iff`
`principal_lt_principal` 📖	mathematical	—	`DedekindCut` `Preorder.toLT` `PartialOrder.toPreorder` `Concept.instPartialOrder` `Preorder.toLE` `principal`	—	—
`principal_sInf_right` 📖	mathematical	—	`principal` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `InfSet.sInf` `CompleteSemilatticeInf.toInfSet` `right`	—	`ext` `Set.ext` `left_principal` `Set.mem_Iic` `le_sInf_iff` `lowerBounds_right` `mem_lowerBounds`
`principal_sSup_left` 📖	mathematical	—	`principal` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `left`	—	`ext'` `Set.ext` `right_principal` `Set.mem_Ici` `sSup_le_iff` `upperBounds_left` `mem_upperBounds`
`right_principal` 📖	mathematical	—	`right` `principal` `Set.Ici`	—	—
`upperBounds_left` 📖	mathematical	—	`upperBounds` `Preorder.toLE` `left` `right`	—	`Concept.upperPolar_extent`

(root)

Definitions

Name	Category	Theorems
`DedekindCut` 📖	CompOp	10 math math: `DedekindCut.principalEmbedding_apply`, `DedekindCut.principalEmbedding_trans_factorEmbedding`, `DedekindCut.coe_principalEmbedding`, `DedekindCut.factorEmbedding_apply`, `DedekindCut.principal_lt_principal`, `DedekindCut.principal_le_principal`, `DedekindCut.factorEmbedding_principal`, `DedekindCut.principalIso_apply`, `DedekindCut.instTotalLe`, `DedekindCut.principalIso_symm_apply`

---

← Back to Index