CompleteSublattice

📁 Source: Mathlib/Order/CompleteSublattice.lean

Statistics

Metric	Count
Definitions `range`, `toOrderIsoRangeOfInjective`, `CompleteSublattice`, `comap`, `copy`, `instBot`, `instCompleteLattice`, `instInfSet`, `instMaxSubtypeMem`, `instMinSubtypeMem`, `instPartialOrder`, `instSetLike`, `instSupSet`, `instTop`, `instTop_1`, `map`, `mk'`, `subtype`, `toSublattice`	19
Theorems `range_coe`, `toOrderIsoRangeOfInjective_apply`, `bot_mem`, `codisjoint_iff`, `coe_bot`, `coe_copy`, `coe_iInf`, `coe_iSup`, `coe_sInf`, `coe_sInf'`, `coe_sSup`, `coe_sSup'`, `coe_subtype`, `coe_top`, `comap_carrier`, `copy_eq`, `disjoint_iff`, `isCompl_iff`, `isComplemented_iff`, `map_carrier`, `mem_comap`, `mem_map`, `mk'_carrier`, `sInfClosed`, `sInfClosed'`, `sSupClosed`, `sSupClosed'`, `subtype_apply`, `subtype_injective`, `top_mem`	30
Total	49

CompleteLatticeHom

Definitions

Name	Category	Theorems
`range` 📖	CompOp	2 math math: `range_coe`, `toOrderIsoRangeOfInjective_apply`
`toOrderIsoRangeOfInjective` 📖	CompOp	1 math math: `toOrderIsoRangeOfInjective_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`range_coe` 📖	mathematical	—	`SetLike.coe` `CompleteSublattice` `CompleteSublattice.instSetLike` `range` `Set.range` `DFunLike.coe` `CompleteLatticeHom` `instFunLike`	—	—
`toOrderIsoRangeOfInjective_apply` 📖	mathematical	`DFunLike.coe` `CompleteLatticeHom` `instFunLike`	`RelIso` `CompleteSublattice` `SetLike.instMembership` `CompleteSublattice.instSetLike` `range` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `RelIso.instFunLike` `toOrderIsoRangeOfInjective` `Set` `Set.instMembership` `Set.range` `RelEmbedding` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `RelEmbedding.instFunLike` `orderEmbeddingOfInjective`	—	—

CompleteSublattice

Definitions

Name	Category	Theorems
`comap` 📖	CompOp	2 math math: `comap_carrier`, `mem_comap`
`copy` 📖	CompOp	2 math math: `copy_eq`, `coe_copy`
`instBot` 📖	CompOp	3 math math: `coe_bot`, `Descriptive.Tree.tree_eq_bot`, `notMem_bot`
`instCompleteLattice` 📖	CompOp	7 math math: `isComplemented_iff`, `mem_subtype`, `codisjoint_iff`, `isCompl_iff`, `subtype_injective`, `coe_subtype`, `disjoint_iff`
`instInfSet` 📖	CompOp	5 math math: `coe_iInf`, `coe_sInf'`, `mem_sInf`, `mem_iInf`, `coe_sInf`
`instMaxSubtypeMem` 📖	CompOp	1 math math: `mem_sup`
`instMinSubtypeMem` 📖	CompOp	1 math math: `mem_inf`
`instPartialOrder` 📖	CompOp	—
`instSetLike` 📖	CompOp	48 math math: `CompleteLatticeHom.range_coe`, `Descriptive.Tree.take_mem`, `isComplemented_iff`, `top_mem`, `Descriptive.Tree.mem_pullSub_long`, `OrderIso.setIsotypicComponents_apply`, `coe_iInf`, `coe_sInf'`, `mem_subtype`, `bot_mem`, `Descriptive.Tree.take_coe`, `Descriptive.Tree.pullSub_adjunction`, `mem_map`, `mem_sInf`, `codisjoint_iff`, `Descriptive.coe_def`, `Descriptive.Tree.pullSub_subAt`, `isCompl_iff`, `Descriptive.Tree.take_eq_take`, `mem_sup`, `coe_sSup'`, `subtype_injective`, `coe_bot`, `mem_fullyInvariantSubmodule_iff`, `mem_inf`, `coe_iSup`, `Descriptive.Tree.tree_eq_bot`, `coe_sSup`, `mem_iSup`, `coe_top`, `mem_top`, `Descriptive.Tree.mem_subAt`, `coe_subtype`, `comap_carrier`, `mem_sSup`, `mem_comap`, `ext_iff`, `CompleteLatticeHom.toOrderIsoRangeOfInjective_apply`, `disjoint_iff`, `mem_iInf`, `OrderIso.setIsotypicComponents_symm_apply`, `Descriptive.Tree.mem_pullSub_self`, `map_carrier`, `Descriptive.Tree.mem_pullSub_short`, `Descriptive.Tree.drop_coe`, `notMem_bot`, `Descriptive.Tree.mem_pullSub_append`, `coe_sInf`
`instSupSet` 📖	CompOp	6 math math: `OrderIso.setIsotypicComponents_apply`, `coe_sSup'`, `coe_iSup`, `coe_sSup`, `mem_iSup`, `mem_sSup`
`instTop` 📖	CompOp	2 math math: `coe_top`, `mem_top`
`instTop_1` 📖	CompOp	—
`map` 📖	CompOp	2 math math: `mem_map`, `map_carrier`
`mk'` 📖	CompOp	1 math math: `mk'_carrier`
`subtype` 📖	CompOp	3 math math: `mem_subtype`, `subtype_injective`, `coe_subtype`
`toSublattice` 📖	CompOp	3 math math: `mk'_carrier`, `comap_carrier`, `map_carrier`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_mem` 📖	mathematical	—	`CompleteSublattice` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`sSup_empty` `sSupClosed'` `Set.empty_subset`
`codisjoint_iff` 📖	mathematical	—	`Codisjoint` `CompleteSublattice` `SetLike.instMembership` `instSetLike` `Subtype.partialOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `BoundedOrder.toOrderTop` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `instCompleteLattice`	—	`codisjoint_iff` `Sublattice.coe_sup` `coe_top` `Subtype.coe_injective`
`coe_bot` 📖	mathematical	—	`CompleteSublattice` `SetLike.instMembership` `instSetLike` `Bot.bot` `instBot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	—
`coe_copy` 📖	mathematical	`SetLike.coe` `CompleteSublattice` `instSetLike`	`copy`	—	—
`coe_iInf` 📖	mathematical	—	`CompleteSublattice` `SetLike.instMembership` `instSetLike` `iInf` `instInfSet` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice`	—	`iInf.eq_1` `coe_sInf'` `iInf_range`
`coe_iSup` 📖	mathematical	—	`CompleteSublattice` `SetLike.instMembership` `instSetLike` `iSup` `instSupSet` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice`	—	`iSup.eq_1` `coe_sSup'` `iSup_range`
`coe_sInf` 📖	mathematical	—	`CompleteSublattice` `SetLike.instMembership` `instSetLike` `InfSet.sInf` `instInfSet` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `setOf` `Set` `Set.instMembership`	—	—
`coe_sInf'` 📖	mathematical	—	`CompleteSublattice` `SetLike.instMembership` `instSetLike` `InfSet.sInf` `instInfSet` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Set` `Set.instMembership`	—	`coe_sInf` `Set.image.eq_1` `sInf_image`
`coe_sSup` 📖	mathematical	—	`CompleteSublattice` `SetLike.instMembership` `instSetLike` `SupSet.sSup` `instSupSet` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `setOf` `Set` `Set.instMembership`	—	—
`coe_sSup'` 📖	mathematical	—	`CompleteSublattice` `SetLike.instMembership` `instSetLike` `SupSet.sSup` `instSupSet` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Set` `Set.instMembership`	—	`coe_sSup` `Set.image.eq_1` `sSup_image`
`coe_subtype` 📖	mathematical	—	`DFunLike.coe` `CompleteLatticeHom` `CompleteSublattice` `SetLike.instMembership` `instSetLike` `instCompleteLattice` `CompleteLatticeHom.instFunLike` `subtype`	—	—
`coe_top` 📖	mathematical	—	`CompleteSublattice` `SetLike.instMembership` `instSetLike` `Top.top` `instTop` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	—
`comap_carrier` 📖	mathematical	—	`Sublattice.carrier` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `toSublattice` `comap` `Set.preimage` `DFunLike.coe` `CompleteLatticeHom` `CompleteLatticeHom.instFunLike` `SetLike.coe` `CompleteSublattice` `instSetLike`	—	—
`copy_eq` 📖	mathematical	`SetLike.coe` `CompleteSublattice` `instSetLike`	`copy`	—	`SetLike.coe_injective`
`disjoint_iff` 📖	mathematical	—	`Disjoint` `CompleteSublattice` `SetLike.instMembership` `instSetLike` `Subtype.partialOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `instCompleteLattice`	—	`disjoint_iff` `Sublattice.coe_inf` `coe_bot` `Subtype.coe_injective`
`isCompl_iff` 📖	mathematical	—	`IsCompl` `CompleteSublattice` `SetLike.instMembership` `instSetLike` `Subtype.partialOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteLattice.toBoundedOrder` `instCompleteLattice`	—	`isCompl_iff` `disjoint_iff` `codisjoint_iff`
`isComplemented_iff` 📖	mathematical	—	`ComplementedLattice` `CompleteSublattice` `SetLike.instMembership` `instSetLike` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `CompleteLattice.toBoundedOrder` `IsCompl` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder`	—	`isCompl_iff`
`map_carrier` 📖	mathematical	—	`Sublattice.carrier` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `toSublattice` `map` `Set.image` `DFunLike.coe` `CompleteLatticeHom` `CompleteLatticeHom.instFunLike` `SetLike.coe` `CompleteSublattice` `instSetLike`	—	—
`mem_comap` 📖	mathematical	—	`CompleteSublattice` `SetLike.instMembership` `instSetLike` `comap` `DFunLike.coe` `CompleteLatticeHom` `CompleteLatticeHom.instFunLike`	—	—
`mem_map` 📖	mathematical	—	`CompleteSublattice` `SetLike.instMembership` `instSetLike` `map` `DFunLike.coe` `CompleteLatticeHom` `CompleteLatticeHom.instFunLike`	—	—
`mk'_carrier` 📖	mathematical	`Set` `Set.instMembership` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	`Sublattice.carrier` `ConditionallyCompleteLattice.toLattice` `toSublattice` `mk'`	—	—
`sInfClosed` 📖	mathematical	`Set` `Set.instHasSubset` `SetLike.coe` `CompleteSublattice` `instSetLike`	`SetLike.instMembership` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice`	—	`sInfClosed'`
`sInfClosed'` 📖	mathematical	`Set` `Set.instHasSubset` `Sublattice.carrier` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `toSublattice`	`Set.instMembership` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder`	—	—
`sSupClosed` 📖	mathematical	`Set` `Set.instHasSubset` `SetLike.coe` `CompleteSublattice` `instSetLike`	`SetLike.instMembership` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice`	—	`sSupClosed'`
`sSupClosed'` 📖	mathematical	`Set` `Set.instHasSubset` `Sublattice.carrier` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `toSublattice`	`Set.instMembership` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder`	—	—
`subtype_apply` 📖	mathematical	—	`DFunLike.coe` `LatticeHom` `Sublattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `SetLike.instMembership` `Sublattice.instSetLike` `Sublattice.instLatticeCoe` `LatticeHom.instFunLike` `Sublattice.subtype`	—	—
`subtype_injective` 📖	mathematical	—	`CompleteSublattice` `SetLike.instMembership` `instSetLike` `DFunLike.coe` `CompleteLatticeHom` `instCompleteLattice` `CompleteLatticeHom.instFunLike` `subtype`	—	`Subtype.coe_injective`
`top_mem` 📖	mathematical	—	`CompleteSublattice` `SetLike.instMembership` `instSetLike` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`sInf_empty` `sInfClosed'` `Set.empty_subset`

(root)

Definitions

Name	Category	Theorems
`CompleteSublattice` 📖	CompData	48 math math: `CompleteLatticeHom.range_coe`, `Descriptive.Tree.take_mem`, `CompleteSublattice.isComplemented_iff`, `CompleteSublattice.top_mem`, `Descriptive.Tree.mem_pullSub_long`, `OrderIso.setIsotypicComponents_apply`, `CompleteSublattice.coe_iInf`, `CompleteSublattice.coe_sInf'`, `CompleteSublattice.mem_subtype`, `CompleteSublattice.bot_mem`, `Descriptive.Tree.take_coe`, `Descriptive.Tree.pullSub_adjunction`, `CompleteSublattice.mem_map`, `CompleteSublattice.mem_sInf`, `CompleteSublattice.codisjoint_iff`, `Descriptive.coe_def`, `Descriptive.Tree.pullSub_subAt`, `CompleteSublattice.isCompl_iff`, `Descriptive.Tree.take_eq_take`, `CompleteSublattice.mem_sup`, `CompleteSublattice.coe_sSup'`, `CompleteSublattice.subtype_injective`, `CompleteSublattice.coe_bot`, `mem_fullyInvariantSubmodule_iff`, `CompleteSublattice.mem_inf`, `CompleteSublattice.coe_iSup`, `Descriptive.Tree.tree_eq_bot`, `CompleteSublattice.coe_sSup`, `CompleteSublattice.mem_iSup`, `CompleteSublattice.coe_top`, `CompleteSublattice.mem_top`, `Descriptive.Tree.mem_subAt`, `CompleteSublattice.coe_subtype`, `CompleteSublattice.comap_carrier`, `CompleteSublattice.mem_sSup`, `CompleteSublattice.mem_comap`, `CompleteSublattice.ext_iff`, `CompleteLatticeHom.toOrderIsoRangeOfInjective_apply`, `CompleteSublattice.disjoint_iff`, `CompleteSublattice.mem_iInf`, `OrderIso.setIsotypicComponents_symm_apply`, `Descriptive.Tree.mem_pullSub_self`, `CompleteSublattice.map_carrier`, `Descriptive.Tree.mem_pullSub_short`, `Descriptive.Tree.drop_coe`, `CompleteSublattice.notMem_bot`, `Descriptive.Tree.mem_pullSub_append`, `CompleteSublattice.coe_sInf`

---

← Back to Index