BooleanSubalgebra

📁 Source: Mathlib/Order/BooleanSubalgebra.lean

Statistics

Metric	Count
Definitions `BooleanSubalgebra`, `closure`, `comap`, `copy`, `inclusion`, `instBooleanAlgebraCoe`, `instBot`, `instBotCoe`, `instComplCoe`, `instCompleteLattice`, `instHImpCoe`, `instInf`, `instInfCoe`, `instInfSet`, `instInhabited`, `instPartialOrder`, `instPartialOrderSubtypeMem`, `instSDiffCoe`, `instSetLike`, `instSupCoe`, `instTop`, `instTopCoe`, `instUniqueOfIsEmpty`, `map`, `subtype`, `toSublattice`, `topEquiv`	27
Theorems `apply_coe_mem_map`, `apply_mem_map_iff`, `biInf_mem`, `biSup_mem`, `bot_mem`, `bot_mem'`, `closure_bot_sup_induction`, `closure_latticeClosure`, `closure_le`, `closure_mono`, `closure_sdiff_sup_induction`, `coe_bot`, `coe_comap`, `coe_copy`, `coe_eq_univ`, `coe_iInf`, `coe_inclusion`, `coe_inf`, `coe_inj`, `coe_map`, `coe_mk`, `coe_sInf`, `coe_subtype`, `coe_top`, `comap_comap`, `comap_equiv_eq_map_symm`, `comap_iInf`, `comap_id`, `comap_inf`, `comap_mono`, `comap_top`, `compl_mem`, `compl_mem'`, `compl_mem_iff`, `compl_mk`, `copy_eq`, `ext`, `gc_map_comap`, `himp_mem`, `iInf_mem`, `iSup_mem`, `inclusion_apply`, `inclusion_injective`, `inclusion_rfl`, `infClosed`, `inf_mem`, `instSubsingletonOfIsEmpty`, `latticeClosure_subset_closure`, `le_comap_iSup`, `le_comap_sup`, `map_bot`, `map_equiv_eq_comap_symm`, `map_iSup`, `map_id`, `map_inf`, `map_inf_le`, `map_le_iff_le_comap`, `map_map`, `map_mono`, `map_sup`, `map_symm_eq_iff_eq_map`, `map_top`, `mem_bot`, `mem_carrier`, `mem_closure`, `mem_closure_iff_sup_sdiff`, `mem_closure_of_mem`, `mem_comap`, `mem_iInf`, `mem_inf`, `mem_map`, `mem_map_equiv`, `mem_map_of_mem`, `mem_mk`, `mem_sInf`, `mem_toSublattice`, `mem_top`, `mk_bot`, `mk_himp_mk`, `mk_inf_mk`, `mk_le_mk`, `mk_lt_mk`, `mk_sdiff_mk`, `mk_sup_mk`, `mk_top`, `sInf_mem`, `sSup_mem`, `sdiff_mem`, `subset_closure`, `subtype_apply`, `subtype_comp_inclusion`, `subtype_injective`, `supClosed`, `sup_mem`, `top_mem`, `val_bot`, `val_compl`, `val_himp`, `val_inf`, `val_sdiff`, `val_sup`, `val_top`	102
Total	129

BooleanSubalgebra

Definitions

Name	Category	Theorems
`closure` 📖	CompOp	8 math math: `closure_mono`, `closure_le`, `latticeClosure_subset_closure`, `mem_closure_iff_sup_sdiff`, `closure_latticeClosure`, `subset_closure`, `mem_closure`, `mem_closure_of_mem`
`comap` 📖	CompOp	14 math math: `map_le_iff_le_comap`, `comap_equiv_eq_map_symm`, `comap_inf`, `mem_comap`, `map_equiv_eq_comap_symm`, `comap_mono`, `comap_id`, `comap_iInf`, `coe_comap`, `le_comap_sup`, `gc_map_comap`, `comap_top`, `le_comap_iSup`, `comap_comap`
`copy` 📖	CompOp	2 math math: `coe_copy`, `copy_eq`
`inclusion` 📖	CompOp	5 math math: `subtype_comp_inclusion`, `coe_inclusion`, `inclusion_injective`, `inclusion_rfl`, `inclusion_apply`
`instBooleanAlgebraCoe` 📖	CompOp	8 math math: `subtype_comp_inclusion`, `subtype_injective`, `coe_inclusion`, `subtype_apply`, `inclusion_injective`, `coe_subtype`, `inclusion_rfl`, `inclusion_apply`
`instBot` 📖	CompOp	3 math math: `coe_bot`, `map_bot`, `mem_bot`
`instBotCoe` 📖	CompOp	2 math math: `val_bot`, `mk_bot`
`instComplCoe` 📖	CompOp	2 math math: `val_compl`, `compl_mk`
`instCompleteLattice` 📖	CompOp	4 math math: `map_iSup`, `map_sup`, `le_comap_sup`, `le_comap_iSup`
`instHImpCoe` 📖	CompOp	2 math math: `mk_himp_mk`, `val_himp`
`instInf` 📖	CompOp	5 math math: `mem_inf`, `comap_inf`, `map_inf_le`, `map_inf`, `coe_inf`
`instInfCoe` 📖	CompOp	2 math math: `mk_inf_mk`, `val_inf`
`instInfSet` 📖	CompOp	5 math math: `mem_iInf`, `coe_iInf`, `mem_sInf`, `comap_iInf`, `coe_sInf`
`instInhabited` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	12 math math: `map_le_iff_le_comap`, `closure_mono`, `comap_mono`, `closure_le`, `map_inf_le`, `mk_le_mk`, `mk_lt_mk`, `map_mono`, `inclusion_rfl`, `le_comap_sup`, `gc_map_comap`, `le_comap_iSup`
`instPartialOrderSubtypeMem` 📖	CompOp	—
`instSDiffCoe` 📖	CompOp	2 math math: `mk_sdiff_mk`, `val_sdiff`
`instSetLike` 📖	CompOp	51 math math: `mem_toSublattice`, `val_bot`, `coe_mk`, `mem_inf`, `top_mem`, `mem_top`, `coe_bot`, `coe_eq_univ`, `coe_top`, `subtype_comp_inclusion`, `mem_comap`, `coe_map`, `compl_mem_iff`, `subtype_injective`, `apply_coe_mem_map`, `apply_mem_map_iff`, `coe_inj`, `closure_le`, `coe_inclusion`, `latticeClosure_subset_closure`, `val_compl`, `mem_closure_iff_sup_sdiff`, `infClosed`, `val_inf`, `subtype_apply`, `inclusion_injective`, `mem_iInf`, `val_sup`, `mem_mk`, `subset_closure`, `mem_map`, `coe_iInf`, `mk_top`, `mem_closure`, `mem_sInf`, `val_sdiff`, `mem_carrier`, `val_top`, `coe_subtype`, `inclusion_rfl`, `coe_sInf`, `coe_inf`, `coe_comap`, `bot_mem`, `val_himp`, `mem_map_equiv`, `inclusion_apply`, `supClosed`, `mem_closure_of_mem`, `mk_bot`, `mem_bot`
`instSupCoe` 📖	CompOp	2 math math: `mk_sup_mk`, `val_sup`
`instTop` 📖	CompOp	5 math math: `mem_top`, `coe_eq_univ`, `coe_top`, `map_top`, `comap_top`
`instTopCoe` 📖	CompOp	2 math math: `mk_top`, `val_top`
`instUniqueOfIsEmpty` 📖	CompOp	—
`map` 📖	CompOp	20 math math: `map_iSup`, `map_le_iff_le_comap`, `map_map`, `comap_equiv_eq_map_symm`, `map_bot`, `coe_map`, `apply_coe_mem_map`, `apply_mem_map_iff`, `map_equiv_eq_comap_symm`, `map_symm_eq_iff_eq_map`, `map_inf_le`, `map_inf`, `mem_map_of_mem`, `map_mono`, `mem_map`, `map_top`, `map_sup`, `mem_map_equiv`, `map_id`, `gc_map_comap`
`subtype` 📖	CompOp	4 math math: `subtype_comp_inclusion`, `subtype_injective`, `subtype_apply`, `coe_subtype`
`toSublattice` 📖	CompOp	3 math math: `mem_toSublattice`, `bot_mem'`, `mem_carrier`
`topEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_coe_mem_map` 📖	mathematical	—	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike` `map` `DFunLike.coe` `BoundedLatticeHom` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `BooleanAlgebra.toBoundedOrder` `BoundedLatticeHom.instFunLike`	—	`mem_map_of_mem` `Subtype.prop`
`apply_mem_map_iff` 📖	mathematical	`DFunLike.coe` `BoundedLatticeHom` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `BooleanAlgebra.toBoundedOrder` `BoundedLatticeHom.instFunLike`	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike` `map`	—	`Function.Injective.mem_set_image`
`biInf_mem` 📖	mathematical	`BooleanSubalgebra` `CompleteBooleanAlgebra.toBooleanAlgebra` `SetLike.instMembership` `instSetLike`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `Set` `Set.instMembership`	—	`InfClosed.biInf_mem` `infClosed` `top_mem`
`biSup_mem` 📖	mathematical	`BooleanSubalgebra` `CompleteBooleanAlgebra.toBooleanAlgebra` `SetLike.instMembership` `instSetLike`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `Set` `Set.instMembership`	—	`SupClosed.biSup_mem` `supClosed` `bot_mem`
`bot_mem` 📖	mathematical	—	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike` `Bot.bot` `BooleanAlgebra.toBot`	—	`bot_mem'`
`bot_mem'` 📖	mathematical	—	`Set` `Set.instMembership` `Sublattice.carrier` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `toSublattice` `Bot.bot` `BooleanAlgebra.toBot`	—	—
`closure_bot_sup_induction` 📖	—	`subset_closure` `Bot.bot` `BooleanAlgebra.toBot` `bot_mem` `closure` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `supClosed` `Compl.compl` `BooleanAlgebra.toCompl` `compl_mem` `BooleanSubalgebra` `SetLike.instMembership` `instSetLike`	—	—	`subset_closure` `bot_mem` `supClosed` `compl_mem` `infClosed` `compl_sup` `compl_compl` `closure_le`
`closure_latticeClosure` 📖	mathematical	—	`closure` `DFunLike.coe` `ClosureOperator` `Set` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `latticeClosure` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra`	—	`le_antisymm` `closure_le` `latticeClosure_subset_closure` `closure_mono` `subset_latticeClosure`
`closure_le` 📖	mathematical	—	`BooleanSubalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_closure` `sInf_le`
`closure_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`BooleanSubalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure`	—	`sInf_le_sInf` `HasSubset.Subset.trans` `Set.instIsTransSubset`
`closure_sdiff_sup_induction` 📖	—	`IsSublattice` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set` `Set.instMembership` `Bot.bot` `BooleanAlgebra.toBot` `Top.top` `BooleanAlgebra.toTop` `BooleanAlgebra.toSDiff` `sdiff_mem` `closure` `subset_closure` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `sup_mem` `BooleanSubalgebra` `SetLike.instMembership` `instSetLike`	—	—	`sdiff_mem` `subset_closure` `sup_mem` `mem_closure_iff_sup_sdiff` `Finset.induction` `Finset.sup_empty` `sdiff_self` `Finset.sup_insert`
`coe_bot` 📖	mathematical	—	`SetLike.coe` `BooleanSubalgebra` `instSetLike` `Bot.bot` `instBot` `Set` `Set.instInsert` `BooleanAlgebra.toBot` `Set.instSingletonSet` `Top.top` `BooleanAlgebra.toTop`	—	—
`coe_comap` 📖	mathematical	—	`SetLike.coe` `BooleanSubalgebra` `instSetLike` `comap` `Set.preimage` `DFunLike.coe` `BoundedLatticeHom` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `BooleanAlgebra.toBoundedOrder` `BoundedLatticeHom.instFunLike`	—	—
`coe_copy` 📖	mathematical	`SetLike.coe` `BooleanSubalgebra` `instSetLike`	`copy`	—	—
`coe_eq_univ` 📖	mathematical	—	`SetLike.coe` `BooleanSubalgebra` `instSetLike` `Set.univ` `Top.top` `instTop`	—	`coe_top`
`coe_iInf` 📖	mathematical	—	`SetLike.coe` `BooleanSubalgebra` `instSetLike` `iInf` `instInfSet` `Set.iInter`	—	`Set.iInter_congr_Prop` `Set.iInter_exists` `Set.iInter_iInter_eq'`
`coe_inclusion` 📖	mathematical	`BooleanSubalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`DFunLike.coe` `BoundedLatticeHom` `SetLike.instMembership` `instSetLike` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instBooleanAlgebraCoe` `BooleanAlgebra.toBoundedOrder` `BoundedLatticeHom.instFunLike` `inclusion` `Set.inclusion` `SetLike.coe`	—	—
`coe_inf` 📖	mathematical	—	`SetLike.coe` `BooleanSubalgebra` `instSetLike` `instInf` `Set` `Set.instInter`	—	—
`coe_inj` 📖	mathematical	—	`SetLike.coe` `BooleanSubalgebra` `instSetLike`	—	`SetLike.coe_set_eq`
`coe_map` 📖	mathematical	—	`SetLike.coe` `BooleanSubalgebra` `instSetLike` `map` `Set.image` `DFunLike.coe` `BoundedLatticeHom` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `BooleanAlgebra.toBoundedOrder` `BoundedLatticeHom.instFunLike`	—	—
`coe_mk` 📖	mathematical	`Set` `Set.instMembership` `Sublattice.carrier` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Compl.compl` `BooleanAlgebra.toCompl` `Bot.bot` `BooleanAlgebra.toBot`	`SetLike.coe` `BooleanSubalgebra` `instSetLike` `Sublattice` `Sublattice.instSetLike`	—	—
`coe_sInf` 📖	mathematical	—	`SetLike.coe` `BooleanSubalgebra` `instSetLike` `InfSet.sInf` `instInfSet` `Set.iInter` `Set` `Set.instMembership`	—	—
`coe_subtype` 📖	mathematical	—	`DFunLike.coe` `BoundedLatticeHom` `BooleanSubalgebra` `SetLike.instMembership` `instSetLike` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instBooleanAlgebraCoe` `BooleanAlgebra.toBoundedOrder` `BoundedLatticeHom.instFunLike` `subtype`	—	—
`coe_top` 📖	mathematical	—	`SetLike.coe` `BooleanSubalgebra` `instSetLike` `Top.top` `instTop` `Set.univ`	—	—
`comap_comap` 📖	mathematical	—	`comap` `BoundedLatticeHom.comp` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `BooleanAlgebra.toBoundedOrder`	—	—
`comap_equiv_eq_map_symm` 📖	mathematical	—	`comap` `map`	—	`OrderIsoClass.toBoundedLatticeHomClass` `OrderIso.instOrderIsoClass` `LatticeHom.map_inf'` `map_equiv_eq_comap_symm`
`comap_iInf` 📖	mathematical	—	`comap` `iInf` `BooleanSubalgebra` `instInfSet`	—	`GaloisConnection.u_iInf` `gc_map_comap`
`comap_id` 📖	mathematical	—	`comap` `BoundedLatticeHom.id` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `BooleanAlgebra.toBoundedOrder`	—	—
`comap_inf` 📖	mathematical	—	`comap` `BooleanSubalgebra` `instInf`	—	`GaloisConnection.u_inf` `gc_map_comap`
`comap_mono` 📖	mathematical	—	`Monotone` `BooleanSubalgebra` `PartialOrder.toPreorder` `instPartialOrder` `comap`	—	`Set.preimage_mono`
`comap_top` 📖	mathematical	—	`comap` `Top.top` `BooleanSubalgebra` `instTop`	—	`GaloisConnection.u_top` `gc_map_comap`
`compl_mem` 📖	mathematical	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike`	`Compl.compl` `BooleanAlgebra.toCompl`	—	`compl_mem'`
`compl_mem'` 📖	mathematical	`Set` `Set.instMembership` `Sublattice.carrier` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `toSublattice`	`Compl.compl` `BooleanAlgebra.toCompl`	—	—
`compl_mem_iff` 📖	mathematical	—	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike` `Compl.compl` `BooleanAlgebra.toCompl`	—	`compl_compl` `compl_mem`
`compl_mk` 📖	mathematical	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike`	`Compl.compl` `instComplCoe` `BooleanAlgebra.toCompl` `compl_mem`	—	—
`copy_eq` 📖	mathematical	`SetLike.coe` `BooleanSubalgebra` `instSetLike`	`copy`	—	`SetLike.coe_injective`
`ext` 📖	—	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike`	—	—	`SetLike.ext`
`gc_map_comap` 📖	mathematical	—	`GaloisConnection` `BooleanSubalgebra` `PartialOrder.toPreorder` `instPartialOrder` `map` `comap`	—	`map_le_iff_le_comap`
`himp_mem` 📖	mathematical	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike`	`HImp.himp` `BooleanAlgebra.toHImp`	—	`himp_eq` `supClosed` `compl_mem`
`iInf_mem` 📖	mathematical	`BooleanSubalgebra` `CompleteBooleanAlgebra.toBooleanAlgebra` `SetLike.instMembership` `instSetLike`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice`	—	`InfClosed.iInf_mem` `infClosed` `top_mem`
`iSup_mem` 📖	mathematical	`BooleanSubalgebra` `CompleteBooleanAlgebra.toBooleanAlgebra` `SetLike.instMembership` `instSetLike`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice`	—	`SupClosed.iSup_mem` `supClosed` `bot_mem`
`inclusion_apply` 📖	mathematical	`BooleanSubalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`DFunLike.coe` `BoundedLatticeHom` `SetLike.instMembership` `instSetLike` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instBooleanAlgebraCoe` `BooleanAlgebra.toBoundedOrder` `BoundedLatticeHom.instFunLike` `inclusion` `Set.inclusion` `SetLike.coe`	—	—
`inclusion_injective` 📖	mathematical	`BooleanSubalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SetLike.instMembership` `instSetLike` `DFunLike.coe` `BoundedLatticeHom` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instBooleanAlgebraCoe` `BooleanAlgebra.toBoundedOrder` `BoundedLatticeHom.instFunLike` `inclusion`	—	`Set.inclusion_injective`
`inclusion_rfl` 📖	mathematical	—	`inclusion` `le_rfl` `BooleanSubalgebra` `PartialOrder.toPreorder` `instPartialOrder` `BoundedLatticeHom.id` `SetLike.instMembership` `instSetLike` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instBooleanAlgebraCoe` `BooleanAlgebra.toBoundedOrder`	—	`le_rfl`
`infClosed` 📖	mathematical	—	`InfClosed` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `SetLike.coe` `BooleanSubalgebra` `instSetLike`	—	`Sublattice.infClosed'`
`inf_mem` 📖	mathematical	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike`	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra`	—	`infClosed`
`instSubsingletonOfIsEmpty` 📖	mathematical	—	`BooleanSubalgebra`	—	`Function.Injective.subsingleton` `SetLike.coe_injective` `Unique.instSubsingleton`
`latticeClosure_subset_closure` 📖	mathematical	—	`Set` `Set.instHasSubset` `DFunLike.coe` `ClosureOperator` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `latticeClosure` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `SetLike.coe` `BooleanSubalgebra` `instSetLike` `closure`	—	`latticeClosure_min` `subset_closure` `Sublattice.isSublattice`
`le_comap_iSup` 📖	mathematical	—	`BooleanSubalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `comap`	—	`Monotone.le_map_iSup` `comap_mono`
`le_comap_sup` 📖	mathematical	—	`BooleanSubalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `comap`	—	`Monotone.le_map_sup` `comap_mono`
`map_bot` 📖	mathematical	—	`map` `Bot.bot` `BooleanSubalgebra` `instBot`	—	`GaloisConnection.l_bot` `gc_map_comap`
`map_equiv_eq_comap_symm` 📖	mathematical	—	`map` `comap`	—	`SetLike.coe_injective` `OrderIsoClass.toBoundedLatticeHomClass` `OrderIso.instOrderIsoClass` `LatticeHom.map_inf'` `Equiv.image_eq_preimage_symm`
`map_iSup` 📖	mathematical	—	`map` `iSup` `BooleanSubalgebra` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`GaloisConnection.l_iSup` `gc_map_comap`
`map_id` 📖	mathematical	—	`map` `BoundedLatticeHom.id` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `BooleanAlgebra.toBoundedOrder`	—	`SetLike.coe_injective` `Set.image_id`
`map_inf` 📖	mathematical	`DFunLike.coe` `BoundedLatticeHom` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `BooleanAlgebra.toBoundedOrder` `BoundedLatticeHom.instFunLike`	`map` `BooleanSubalgebra` `instInf`	—	`SetLike.coe_set_eq` `Set.image_inter`
`map_inf_le` 📖	mathematical	—	`BooleanSubalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `map` `instInf`	—	`Monotone.map_inf_le` `map_mono`
`map_le_iff_le_comap` 📖	mathematical	—	`BooleanSubalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `map` `comap`	—	`Set.image_subset_iff`
`map_map` 📖	mathematical	—	`map` `BoundedLatticeHom.comp` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `BooleanAlgebra.toBoundedOrder`	—	`SetLike.coe_injective` `Set.image_image`
`map_mono` 📖	mathematical	—	`Monotone` `BooleanSubalgebra` `PartialOrder.toPreorder` `instPartialOrder` `map`	—	`Set.image_mono`
`map_sup` 📖	mathematical	—	`map` `BooleanSubalgebra` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`GaloisConnection.l_sup` `gc_map_comap`
`map_symm_eq_iff_eq_map` 📖	mathematical	—	`map`	—	`OrderIsoClass.toBoundedLatticeHomClass` `OrderIso.instOrderIsoClass` `LatticeHom.map_inf'` `Equiv.eq_image_iff_symm_image_eq`
`map_top` 📖	mathematical	`DFunLike.coe` `BoundedLatticeHom` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `BooleanAlgebra.toBoundedOrder` `BoundedLatticeHom.instFunLike`	`map` `Top.top` `BooleanSubalgebra` `instTop`	—	`SetLike.coe_injective` `Set.image_univ` `Function.Surjective.range_eq`
`mem_bot` 📖	mathematical	—	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike` `Bot.bot` `instBot` `BooleanAlgebra.toBot` `Top.top` `BooleanAlgebra.toTop`	—	—
`mem_carrier` 📖	mathematical	—	`Set` `Set.instMembership` `Sublattice.carrier` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `toSublattice` `BooleanSubalgebra` `SetLike.instMembership` `instSetLike`	—	—
`mem_closure` 📖	mathematical	—	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike` `closure`	—	`mem_sInf`
`mem_closure_iff_sup_sdiff` 📖	mathematical	`IsSublattice` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set` `Set.instMembership` `Bot.bot` `BooleanAlgebra.toBot` `Top.top` `BooleanAlgebra.toTop`	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike` `closure` `Finset.sup` `Set.Elem` `Lattice.toSemilatticeSup` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `BooleanAlgebra.toSDiff`	—	`closure_bot_sup_induction` `Finset.sup_singleton` `sdiff_bot` `Finset.sup_empty` `Finset.sup_union` `Finset.induction` `compl_bot` `Finset.sup_insert` `compl_sup` `inf_of_le_right` `inf_sup_left` `IsSublattice.supClosed` `IsSublattice.infClosed` `sdiff_eq` `inf_left_comm` `compl_inf` `compl_compl` `inf_sup_right` `inf_assoc` `Finset.sup_mem` `subset_closure` `sup_mem` `sdiff_mem`
`mem_closure_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike` `closure`	—	`subset_closure`
`mem_comap` 📖	mathematical	—	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike` `comap` `DFunLike.coe` `BoundedLatticeHom` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `BooleanAlgebra.toBoundedOrder` `BoundedLatticeHom.instFunLike`	—	—
`mem_iInf` 📖	mathematical	—	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike` `iInf` `instInfSet`	—	`SetLike.mem_coe` `coe_iInf`
`mem_inf` 📖	mathematical	—	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike` `instInf`	—	—
`mem_map` 📖	mathematical	—	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike` `map` `DFunLike.coe` `BoundedLatticeHom` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `BooleanAlgebra.toBoundedOrder` `BoundedLatticeHom.instFunLike`	—	—
`mem_map_equiv` 📖	mathematical	—	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike` `map` `DFunLike.coe` `OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instFunLikeOrderIso` `OrderIso.symm`	—	`Set.mem_image_equiv`
`mem_map_of_mem` 📖	mathematical	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike`	`map` `DFunLike.coe` `BoundedLatticeHom` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `BooleanAlgebra.toBoundedOrder` `BoundedLatticeHom.instFunLike`	—	`Set.mem_image_of_mem`
`mem_mk` 📖	mathematical	`Set` `Set.instMembership` `Sublattice.carrier` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Compl.compl` `BooleanAlgebra.toCompl` `Bot.bot` `BooleanAlgebra.toBot`	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike` `Sublattice` `Sublattice.instSetLike`	—	—
`mem_sInf` 📖	mathematical	—	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike` `InfSet.sInf` `instInfSet`	—	`SetLike.mem_coe`
`mem_toSublattice` 📖	mathematical	—	`Sublattice` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `SetLike.instMembership` `Sublattice.instSetLike` `toSublattice` `BooleanSubalgebra` `instSetLike`	—	—
`mem_top` 📖	mathematical	—	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike` `Top.top` `instTop`	—	`Set.mem_univ`
`mk_bot` 📖	mathematical	—	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike` `Bot.bot` `BooleanAlgebra.toBot` `bot_mem` `instBotCoe`	—	`bot_mem`
`mk_himp_mk` 📖	mathematical	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike`	`HImp.himp` `instHImpCoe` `BooleanAlgebra.toHImp` `himp_mem`	—	—
`mk_inf_mk` 📖	mathematical	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike`	`instInfCoe` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `infClosed`	—	—
`mk_le_mk` 📖	mathematical	`Set` `Set.instMembership` `Sublattice.carrier` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Compl.compl` `BooleanAlgebra.toCompl` `Bot.bot` `BooleanAlgebra.toBot`	`BooleanSubalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Sublattice` `Sublattice.instPartialOrder`	—	—
`mk_lt_mk` 📖	mathematical	`Set` `Set.instMembership` `Sublattice.carrier` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Compl.compl` `BooleanAlgebra.toCompl` `Bot.bot` `BooleanAlgebra.toBot`	`BooleanSubalgebra` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `Sublattice` `Sublattice.instPartialOrder`	—	—
`mk_sdiff_mk` 📖	mathematical	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike`	`instSDiffCoe` `BooleanAlgebra.toSDiff` `sdiff_mem`	—	—
`mk_sup_mk` 📖	mathematical	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike`	`instSupCoe` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `supClosed`	—	—
`mk_top` 📖	mathematical	—	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike` `Top.top` `BooleanAlgebra.toTop` `top_mem` `instTopCoe`	—	`top_mem`
`sInf_mem` 📖	mathematical	`Set` `Set.instHasSubset` `SetLike.coe` `BooleanSubalgebra` `CompleteBooleanAlgebra.toBooleanAlgebra` `instSetLike`	`SetLike.instMembership` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice`	—	`InfClosed.sInf_mem` `infClosed` `top_mem`
`sSup_mem` 📖	mathematical	`Set` `Set.instHasSubset` `SetLike.coe` `BooleanSubalgebra` `CompleteBooleanAlgebra.toBooleanAlgebra` `instSetLike`	`SetLike.instMembership` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice`	—	`SupClosed.sSup_mem` `supClosed` `bot_mem`
`sdiff_mem` 📖	mathematical	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike`	`BooleanAlgebra.toSDiff`	—	`sdiff_eq` `infClosed` `compl_mem`
`subset_closure` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `BooleanSubalgebra` `instSetLike` `closure`	—	`mem_closure`
`subtype_apply` 📖	mathematical	—	`DFunLike.coe` `BoundedLatticeHom` `BooleanSubalgebra` `SetLike.instMembership` `instSetLike` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instBooleanAlgebraCoe` `BooleanAlgebra.toBoundedOrder` `BoundedLatticeHom.instFunLike` `subtype`	—	—
`subtype_comp_inclusion` 📖	mathematical	`BooleanSubalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`BoundedLatticeHom.comp` `SetLike.instMembership` `instSetLike` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instBooleanAlgebraCoe` `BooleanAlgebra.toBoundedOrder` `subtype` `inclusion`	—	—
`subtype_injective` 📖	mathematical	—	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike` `DFunLike.coe` `BoundedLatticeHom` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instBooleanAlgebraCoe` `BooleanAlgebra.toBoundedOrder` `BoundedLatticeHom.instFunLike` `subtype`	—	`Subtype.coe_injective`
`supClosed` 📖	mathematical	—	`SupClosed` `Lattice.toSemilatticeSup` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `SetLike.coe` `BooleanSubalgebra` `instSetLike`	—	`Sublattice.supClosed'`
`sup_mem` 📖	mathematical	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike`	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra`	—	`supClosed`
`top_mem` 📖	mathematical	—	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike` `Top.top` `BooleanAlgebra.toTop`	—	`compl_bot` `compl_mem` `bot_mem`
`val_bot` 📖	mathematical	—	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike` `Bot.bot` `instBotCoe` `BooleanAlgebra.toBot`	—	—
`val_compl` 📖	mathematical	—	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike` `Compl.compl` `instComplCoe` `BooleanAlgebra.toCompl`	—	—
`val_himp` 📖	mathematical	—	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike` `HImp.himp` `instHImpCoe` `BooleanAlgebra.toHImp`	—	—
`val_inf` 📖	mathematical	—	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike` `instInfCoe` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra`	—	—
`val_sdiff` 📖	mathematical	—	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike` `instSDiffCoe` `BooleanAlgebra.toSDiff`	—	—
`val_sup` 📖	mathematical	—	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike` `instSupCoe` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra`	—	—
`val_top` 📖	mathematical	—	`BooleanSubalgebra` `SetLike.instMembership` `instSetLike` `Top.top` `instTopCoe` `BooleanAlgebra.toTop`	—	—

(root)

Definitions

Name	Category	Theorems
`BooleanSubalgebra` 📖	CompData	66 math math: `BooleanSubalgebra.map_iSup`, `BooleanSubalgebra.mem_toSublattice`, `BooleanSubalgebra.val_bot`, `BooleanSubalgebra.coe_mk`, `BooleanSubalgebra.map_le_iff_le_comap`, `BooleanSubalgebra.mem_inf`, `BooleanSubalgebra.comap_inf`, `BooleanSubalgebra.instSubsingletonOfIsEmpty`, `BooleanSubalgebra.top_mem`, `BooleanSubalgebra.mem_top`, `BooleanSubalgebra.coe_bot`, `BooleanSubalgebra.coe_eq_univ`, `BooleanSubalgebra.coe_top`, `BooleanSubalgebra.map_bot`, `BooleanSubalgebra.mem_comap`, `BooleanSubalgebra.coe_map`, `BooleanSubalgebra.compl_mem_iff`, `BooleanSubalgebra.subtype_injective`, `BooleanSubalgebra.apply_coe_mem_map`, `BooleanSubalgebra.closure_mono`, `BooleanSubalgebra.apply_mem_map_iff`, `BooleanSubalgebra.comap_mono`, `BooleanSubalgebra.coe_inj`, `BooleanSubalgebra.closure_le`, `BooleanSubalgebra.map_inf_le`, `BooleanSubalgebra.mk_le_mk`, `BooleanSubalgebra.latticeClosure_subset_closure`, `BooleanSubalgebra.val_compl`, `BooleanSubalgebra.mem_closure_iff_sup_sdiff`, `BooleanSubalgebra.infClosed`, `BooleanSubalgebra.map_inf`, `BooleanSubalgebra.val_inf`, `BooleanSubalgebra.subtype_apply`, `BooleanSubalgebra.mk_lt_mk`, `BooleanSubalgebra.mem_iInf`, `BooleanSubalgebra.val_sup`, `BooleanSubalgebra.mem_mk`, `BooleanSubalgebra.map_mono`, `BooleanSubalgebra.subset_closure`, `BooleanSubalgebra.mem_map`, `BooleanSubalgebra.coe_iInf`, `BooleanSubalgebra.mk_top`, `BooleanSubalgebra.mem_closure`, `BooleanSubalgebra.mem_sInf`, `BooleanSubalgebra.comap_iInf`, `BooleanSubalgebra.val_sdiff`, `BooleanSubalgebra.map_top`, `BooleanSubalgebra.mem_carrier`, `BooleanSubalgebra.val_top`, `BooleanSubalgebra.coe_subtype`, `BooleanSubalgebra.inclusion_rfl`, `BooleanSubalgebra.coe_sInf`, `BooleanSubalgebra.coe_inf`, `BooleanSubalgebra.coe_comap`, `BooleanSubalgebra.bot_mem`, `BooleanSubalgebra.val_himp`, `BooleanSubalgebra.map_sup`, `BooleanSubalgebra.mem_map_equiv`, `BooleanSubalgebra.le_comap_sup`, `BooleanSubalgebra.gc_map_comap`, `BooleanSubalgebra.supClosed`, `BooleanSubalgebra.comap_top`, `BooleanSubalgebra.le_comap_iSup`, `BooleanSubalgebra.mem_closure_of_mem`, `BooleanSubalgebra.mk_bot`, `BooleanSubalgebra.mem_bot`

---

← Back to Index