Closeds

📁 Source: Mathlib/Topology/Sets/Closeds.lean

Statistics

Metric	Count
Definitions `Clopens`, `carrier`, `instBooleanAlgebra`, `instBot`, `instCompl`, `instHImp`, `instInhabited`, `instMax`, `instMin`, `instPartialOrder`, `instSDiff`, `instSProdProd`, `instSetLike`, `instTop`, `toCloseds`, `toOpens`, `carrier`, `closure`, `coframeMinimalAxioms`, `compl`, `complOrderIso`, `gi`, `instCoframe`, `instCompleteLattice`, `instInhabited`, `instPartialOrder`, `instSetLike`, `instSingletonOfT1Space`, `preimage`, `singleton`, `IrreducibleCloseds`, `carrier`, `equivSubtype`, `equivSubtype'`, `instPartialOrder`, `instSetLike`, `instSingletonOfT1Space`, `map`, `orderIsoSubtype`, `orderIsoSubtype'`, `singleton`, `compl`, `complOrderIso`	43
Theorems `coe_bot`, `coe_compl`, `coe_disjoint`, `coe_finset_sup`, `coe_himp`, `coe_inf`, `coe_mk`, `coe_sdiff`, `coe_sup`, `coe_toCloseds`, `coe_toOpens`, `coe_top`, `ext`, `ext_iff`, `isClopen`, `isClopen'`, `isClosed`, `isOpen`, `mem_mk`, `mem_prod`, `carrier_eq_coe`, `closure_le`, `coe_bot`, `coe_closure`, `coe_compl`, `coe_eq_empty`, `coe_eq_singleton_of_isAtom`, `coe_eq_univ`, `coe_finset_inf`, `coe_finset_sup`, `coe_iInf`, `coe_inf`, `coe_mk`, `coe_nonempty`, `coe_preimage`, `coe_sInf`, `coe_sSup`, `coe_singleton`, `coe_sup`, `coe_top`, `complOrderIso_apply`, `complOrderIso_symm_apply`, `compl_bijective`, `compl_compl`, `ext`, `ext_iff`, `gc`, `iInf_def`, `iInf_mk`, `instCanLiftSetCoeIsClosed`, `isAtom_coe`, `isAtom_iff`, `isClosed`, `isClosed'`, `mem_closure`, `mem_iInf`, `mem_mk`, `mem_sInf`, `mem_singleton`, `mk_singleton`, `singleton_inj`, `singleton_injective`, `coe_map`, `coe_mk`, `coe_singleton`, `equivSubtype'_apply`, `equivSubtype'_symm_apply`, `equivSubtype_apply`, `equivSubtype_symm_apply`, `ext`, `ext_iff`, `instCanLiftSetCoeAndIsIrreducibleIsClosed`, `isClosed`, `isClosed'`, `isIrreducible`, `isIrreducible'`, `is_closed'`, `is_irreducible'`, `map_injective_of_isInducing`, `map_mono`, `map_strictMono_of_isInducing`, `mem_singleton`, `mk_singleton`, `singleton_inj`, `singleton_injective`, `coe_compl`, `complOrderIso_apply`, `complOrderIso_symm_apply`, `compl_bijective`, `compl_compl`, `isCoatom_iff`	91
Total	134

TopologicalSpace

Definitions

Name	Category	Theorems
`Clopens` 📖	CompData	43 math math: `Clopens.coe_mk`, `Clopens.coe_bot`, `LightProfinite.instCountableClopensCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology`, `Clopens.ext_iff`, `DiscreteQuotient.finsetClopens_inj`, `CompactOpens.coe_toClopens`, `PrimeSpectrum.isIdempotentElemEquivClopens_symm_bot`, `PrimeSpectrum.isIdempotentElemEquivClopens_one_sub`, `Clopens.coe_disjoint`, `ClopenUpperSet.coe_mk`, `Clopens.isClopen`, `PrimeSpectrum.isIdempotentElemEquivClopens_symm_inf`, `Clopens.finite_prod`, `Clopens.coe_sdiff`, `ContinuousMap.exists_finite_sum_const_indicator_approximation_of_mem_nhds_diagonal`, `Clopens.coe_top`, `Clopens.exists_finset_eq_sup_prod`, `Clopens.coe_inf`, `DiscreteQuotient.comp_finsetClopens`, `Clopens.mem_mk`, `PrimeSpectrum.isIdempotentElemEquivClopens_symm_sup`, `Clopens.isOpen`, `Clopens.coe_sup`, `ContinuousMap.exists_finite_sum_const_mulIndicator_approximation_of_mem_nhds_diagonal`, `Clopens.coe_compl`, `PrimeSpectrum.isIdempotentElemEquivClopens_apply_toOpens`, `PrimeSpectrum.basicOpen_isIdempotentElemEquivClopens_symm`, `Clopens.isClosed`, `Clopens.surjective_finset_sup_prod`, `Clopens.coe_himp`, `Clopens.coe_finset_sup`, `Clopens.coe_toCloseds`, `PrimeSpectrum.isIdempotentElemEquivClopens_symm_top`, `Clopens.coe_toOpens`, `Clopens.countable_prod`, `Clopens.countable_iff_secondCountable`, `IsOpenCover.exists_finite_clopen_cover`, `ContinuousMap.exists_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal`, `Clopens.mem_prod`, `PrimeSpectrum.isIdempotentElemEquivClopens_mul`, `PrimeSpectrum.coe_isIdempotentElemEquivClopens_apply`, `PrimeSpectrum.isIdempotentElemEquivClopens_symm_compl`, `IsOpenCover.exists_finite_nonempty_disjoint_clopen_cover`
`IrreducibleCloseds` 📖	CompData	20 math math: `IrreducibleCloseds.coe_mk`, `IrreducibleCloseds.map_strictMono_of_isInducing`, `IrreducibleCloseds.singleton_inj`, `IrreducibleCloseds.instCanLiftSetCoeAndIsIrreducibleIsClosed`, `IrreducibleCloseds.singleton_injective`, `IrreducibleCloseds.is_irreducible'`, `IrreducibleCloseds.isIrreducible`, `IrreducibleCloseds.isClosed`, `IrreducibleCloseds.is_closed'`, `IrreducibleCloseds.coe_singleton`, `IrreducibleCloseds.equivSubtype_apply`, `IrreducibleCloseds.mem_singleton`, `IrreducibleCloseds.map_injective_of_isInducing`, `IrreducibleCloseds.map_mono`, `IrreducibleCloseds.ext_iff`, `IrreducibleCloseds.equivSubtype'_apply`, `IrreducibleCloseds.coe_map`, `IrreducibleCloseds.equivSubtype_symm_apply`, `IrreducibleCloseds.mk_singleton`, `IrreducibleCloseds.equivSubtype'_symm_apply`

TopologicalSpace.Clopens

Definitions

Name	Category	Theorems
`carrier` 📖	CompOp	3 math math: `DiscreteQuotient.comp_finsetClopens`, `isClopen'`, `ClopenUpperSet.upper'`
`instBooleanAlgebra` 📖	CompOp	6 math math: `coe_disjoint`, `exists_finset_eq_sup_prod`, `surjective_finset_sup_prod`, `coe_finset_sup`, `ContinuousMap.exists_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal`, `TopologicalSpace.IsOpenCover.exists_finite_nonempty_disjoint_clopen_cover`
`instBot` 📖	CompOp	2 math math: `coe_bot`, `PrimeSpectrum.isIdempotentElemEquivClopens_symm_bot`
`instCompl` 📖	CompOp	3 math math: `PrimeSpectrum.isIdempotentElemEquivClopens_one_sub`, `coe_compl`, `PrimeSpectrum.isIdempotentElemEquivClopens_symm_compl`
`instHImp` 📖	CompOp	1 math math: `coe_himp`
`instInhabited` 📖	CompOp	—
`instMax` 📖	CompOp	2 math math: `PrimeSpectrum.isIdempotentElemEquivClopens_symm_sup`, `coe_sup`
`instMin` 📖	CompOp	3 math math: `PrimeSpectrum.isIdempotentElemEquivClopens_symm_inf`, `coe_inf`, `PrimeSpectrum.isIdempotentElemEquivClopens_mul`
`instPartialOrder` 📖	CompOp	14 math math: `exists_prod_subset`, `PrimeSpectrum.isIdempotentElemEquivClopens_symm_bot`, `PrimeSpectrum.isIdempotentElemEquivClopens_one_sub`, `coe_disjoint`, `PrimeSpectrum.isIdempotentElemEquivClopens_symm_inf`, `PrimeSpectrum.isIdempotentElemEquivClopens_symm_sup`, `PrimeSpectrum.isIdempotentElemEquivClopens_apply_toOpens`, `PrimeSpectrum.basicOpen_isIdempotentElemEquivClopens_symm`, `PrimeSpectrum.isIdempotentElemEquivClopens_symm_top`, `ContinuousMap.exists_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal`, `PrimeSpectrum.isIdempotentElemEquivClopens_mul`, `PrimeSpectrum.coe_isIdempotentElemEquivClopens_apply`, `PrimeSpectrum.isIdempotentElemEquivClopens_symm_compl`, `TopologicalSpace.IsOpenCover.exists_finite_nonempty_disjoint_clopen_cover`
`instSDiff` 📖	CompOp	1 math math: `coe_sdiff`
`instSProdProd` 📖	CompOp	4 math math: `exists_prod_subset`, `exists_finset_eq_sup_prod`, `surjective_finset_sup_prod`, `mem_prod`
`instSetLike` 📖	CompOp	26 math math: `coe_mk`, `coe_bot`, `ext_iff`, `TopologicalSpace.CompactOpens.coe_toClopens`, `coe_disjoint`, `ClopenUpperSet.coe_mk`, `isClopen`, `coe_sdiff`, `ContinuousMap.exists_finite_sum_const_indicator_approximation_of_mem_nhds_diagonal`, `coe_top`, `coe_inf`, `mem_mk`, `isOpen`, `coe_sup`, `ContinuousMap.exists_finite_sum_const_mulIndicator_approximation_of_mem_nhds_diagonal`, `coe_compl`, `isClosed`, `coe_himp`, `coe_finset_sup`, `coe_toCloseds`, `coe_toOpens`, `TopologicalSpace.IsOpenCover.exists_finite_clopen_cover`, `ContinuousMap.exists_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal`, `mem_prod`, `PrimeSpectrum.coe_isIdempotentElemEquivClopens_apply`, `TopologicalSpace.IsOpenCover.exists_finite_nonempty_disjoint_clopen_cover`
`instTop` 📖	CompOp	2 math math: `coe_top`, `PrimeSpectrum.isIdempotentElemEquivClopens_symm_top`
`toCloseds` 📖	CompOp	1 math math: `coe_toCloseds`
`toOpens` 📖	CompOp	3 math math: `PrimeSpectrum.isIdempotentElemEquivClopens_apply_toOpens`, `PrimeSpectrum.basicOpen_isIdempotentElemEquivClopens_symm`, `coe_toOpens`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_bot` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Clopens` `instSetLike` `Bot.bot` `instBot` `Set` `Set.instEmptyCollection`	—	—
`coe_compl` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Clopens` `instSetLike` `Compl.compl` `instCompl` `Set` `Set.instCompl`	—	—
`coe_disjoint` 📖	mathematical	—	`Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `TopologicalSpace.Clopens` `instSetLike` `instPartialOrder` `BiheytingAlgebra.toHeytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instBooleanAlgebra`	—	—
`coe_finset_sup` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Clopens` `instSetLike` `Finset.sup` `Lattice.toSemilatticeSup` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `Set.iUnion` `Finset` `Finset.instMembership`	—	`Finset.induction_on` `Finset.sup_empty` `Set.iUnion_congr_Prop` `Set.iUnion_of_empty` `instIsEmptyFalse` `Set.iUnion_empty` `Finset.sup_insert` `Set.iUnion_iUnion_eq_or_left`
`coe_himp` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Clopens` `instSetLike` `HImp.himp` `instHImp` `Set` `BooleanAlgebra.toHImp` `Set.instBooleanAlgebra`	—	—
`coe_inf` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Clopens` `instSetLike` `instMin` `Set` `Set.instInter`	—	—
`coe_mk` 📖	mathematical	`IsClopen`	`SetLike.coe` `TopologicalSpace.Clopens` `instSetLike`	—	—
`coe_sdiff` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Clopens` `instSetLike` `instSDiff` `Set` `Set.instSDiff`	—	—
`coe_sup` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Clopens` `instSetLike` `instMax` `Set` `Set.instUnion`	—	—
`coe_toCloseds` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Closeds` `TopologicalSpace.Closeds.instSetLike` `toCloseds` `TopologicalSpace.Clopens` `instSetLike`	—	—
`coe_toOpens` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Opens` `TopologicalSpace.Opens.instSetLike` `toOpens` `TopologicalSpace.Clopens` `instSetLike`	—	—
`coe_top` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Clopens` `instSetLike` `Top.top` `instTop` `Set.univ`	—	—
`ext` 📖	—	`SetLike.coe` `TopologicalSpace.Clopens` `instSetLike`	—	—	`SetLike.ext'`
`ext_iff` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Clopens` `instSetLike`	—	`ext`
`isClopen` 📖	mathematical	—	`IsClopen` `SetLike.coe` `TopologicalSpace.Clopens` `instSetLike`	—	`isClopen'`
`isClopen'` 📖	mathematical	—	`IsClopen` `carrier`	—	—
`isClosed` 📖	mathematical	—	`IsClosed` `SetLike.coe` `TopologicalSpace.Clopens` `instSetLike`	—	`IsClopen.isClosed` `isClopen`
`isOpen` 📖	mathematical	—	`IsOpen` `SetLike.coe` `TopologicalSpace.Clopens` `instSetLike`	—	`IsClopen.isOpen` `isClopen`
`mem_mk` 📖	mathematical	`IsClopen`	`TopologicalSpace.Clopens` `SetLike.instMembership` `instSetLike` `Set` `Set.instMembership`	—	—
`mem_prod` 📖	mathematical	—	`TopologicalSpace.Clopens` `instTopologicalSpaceProd` `SetLike.instMembership` `instSetLike` `SProd.sprod` `instSProdProd`	—	—

TopologicalSpace.Closeds

Definitions

Name	Category	Theorems
`carrier` 📖	CompOp	2 math math: `carrier_eq_coe`, `isClosed'`
`closure` 📖	CompOp	10 math math: `uniformContinuous_closure`, `closure_le`, `gc`, `continuous_closure`, `AlgebraicGeometry.Scheme.IdealSheafData.map_vanishingIdeal`, `PrimitiveSpectrum.closedsGC_closureOperator`, `AlgebraicGeometry.Scheme.IdealSheafData.support_map`, `mem_closure`, `coe_closure`, `isUniformInducing_closure`
`coframeMinimalAxioms` 📖	CompOp	—
`compl` 📖	CompOp	7 math math: `coe_compl`, `TopologicalSpace.Opens.isCoatom_iff`, `TopologicalSpace.Opens.complOrderIso_symm_apply`, `compl_compl`, `complOrderIso_apply`, `compl_bijective`, `TopologicalSpace.Opens.compl_compl`
`complOrderIso` 📖	CompOp	2 math math: `complOrderIso_symm_apply`, `complOrderIso_apply`
`gi` 📖	CompOp	—
`instCoframe` 📖	CompOp	4 math math: `AlgebraicGeometry.Scheme.support_nilradical`, `AlgebraicGeometry.Scheme.IdealSheafData.support_eq_top_iff`, `AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_top`, `AlgebraicGeometry.Scheme.IdealSheafData.support_bot`
`instCompleteLattice` 📖	CompOp	35 math math: `iInf_def`, `AlgebraicGeometry.Scheme.IdealSheafData.support_mul`, `coe_iInf`, `instContinuousSup`, `coe_eq_empty`, `TopologicalSpace.NoetherianSpace.exists_finset_irreducible`, `UniformContinuous.sup_closeds`, `mem_sInf`, `lipschitz_sup`, `coe_bot`, `coe_finset_inf`, `AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_sup`, `AlgebraicGeometry.Scheme.IdealSheafData.support_eq_bot_iff`, `isAtom_iff`, `AlgebraicGeometry.Scheme.IdealSheafData.support_iSup`, `coe_inf`, `coe_sup`, `coe_top`, `coe_finset_sup`, `coe_eq_univ`, `TopologicalSpace.NoetherianSpace.exists_finite_set_closeds_irreducible`, `coe_sSup`, `isClopen_singleton_bot`, `iInf_mk`, `isAtom_coe`, `EMetric.Closeds.lipschitz_sup`, `uniformContinuous_sup`, `AlgebraicGeometry.Scheme.IdealSheafData.support_top`, `coe_sInf`, `AlgebraicGeometry.Scheme.IdealSheafData.support_sup`, `mem_iInf`, `AlgebraicGeometry.Scheme.IdealSheafData.support_sSup`, `AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_iSup`, `AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_sSup`, `AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_bot`
`instInhabited` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	14 math math: `complOrderIso_symm_apply`, `AlgebraicGeometry.Scheme.IdealSheafData.gc`, `TopologicalSpace.Opens.complOrderIso_apply`, `closure_le`, `TopologicalSpace.Opens.complOrderIso_symm_apply`, `gc`, `complOrderIso_apply`, `AlgebraicGeometry.Scheme.IdealSheafData.le_support_iff_le_vanishingIdeal`, `AlgebraicGeometry.Scheme.IdealSheafData.support_antitone`, `isAtom_iff`, `TopologicalSpace.noetherianSpace_TFAE`, `PrimitiveSpectrum.closedsGC_closureOperator`, `TopologicalSpace.instWellFoundedLTClosedsOfNoetherianSpace`, `isAtom_coe`
`instSetLike` 📖	CompOp	71 math math: `iInf_def`, `coe_compl`, `isClosed`, `AlgebraicGeometry.Scheme.Hom.iUnion_support_ker_openCover_map_comp`, `mem_singleton`, `TopologicalSpace.Compacts.coe_toCloseds`, `isUniformEmbedding_coe`, `coe_iInf`, `ext_iff`, `closure_le`, `coe_eq_empty`, `AlgebraicGeometry.Scheme.IdealSheafData.coe_support_mkOfMemSupportIff`, `TopologicalSpace.NoetherianSpace.exists_finset_irreducible`, `coe_preimage`, `gc`, `Filter.HasBasis.uniformity_closeds`, `AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι_eq_support_inter`, `uniformity_def`, `AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff_of_mem`, `TopologicalSpace.NonemptyCompacts.mem_toCloseds`, `TopologicalSpace.NonemptyCompacts.coe_toCloseds`, `AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_ideal`, `mem_sInf`, `coe_singleton`, `AlgebraicGeometry.Scheme.IdealSheafData.range_subschemeι`, `AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff`, `EMetric.isClosed_subsets_of_isClosed`, `AlgebraicGeometry.Scheme.IdealSheafData.coe_support_ofIdealTop`, `coe_bot`, `edist_eq`, `AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff_mem_support`, `coe_finset_inf`, `ClosedSubmodule.coe_toCloseds`, `TopologicalSpace.Compacts.mem_toCloseds`, `isClosed_subsets_of_isClosed`, `coe_nonempty`, `continuous_infEDist`, `AlgebraicGeometry.Scheme.IdealSheafData.map_vanishingIdeal`, `coe_inf`, `carrier_eq_coe`, `coe_sup`, `coe_top`, `PrimitiveSpectrum.closedsGC_closureOperator`, `coe_finset_sup`, `coe_eq_univ`, `TopologicalSpace.NoetherianSpace.exists_finite_set_closeds_irreducible`, `coe_mk`, `coe_sSup`, `AlgebraicGeometry.Scheme.IdealSheafData.coe_support_eq_eq_iInter_zeroLocus`, `TopologicalSpace.Opens.coe_compl`, `AlgebraicGeometry.Scheme.IdealSheafData.support_map`, `TopologicalSpace.Clopens.coe_toCloseds`, `isAtom_coe`, `mem_closure`, `totallyBounded_subsets_of_totallyBounded`, `AlgebraicGeometry.Scheme.Hom.range_subset_ker_support`, `AlgebraicGeometry.Scheme.IdealSheafData.coe_support_inter`, `AlgebraicGeometry.Scheme.Hom.support_ker`, `coe_closure`, `uniformContinuous_coe`, `mem_mk`, `EMetric.Closeds.edist_eq`, `coe_sInf`, `AlgebraicGeometry.Scheme.IdealSheafData.coe_support_vanishingIdeal`, `EMetric.Closeds.isClosed_subsets_of_isClosed`, `mem_iInf`, `coe_eq_singleton_of_isAtom`, `instCanLiftSetCoeIsClosed`, `EMetric.continuous_infEdist_hausdorffEdist`, `AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_apply`, `isOpen_inter_nonempty_of_isOpen`
`instSingletonOfT1Space` 📖	CompOp	16 math math: `TopologicalSpace.Compacts.toCloseds_singleton`, `mem_singleton`, `TopologicalSpace.Opens.isCoatom_iff`, `EMetric.Closeds.isometry_singleton`, `singleton_inj`, `mk_singleton`, `singleton_injective`, `coe_singleton`, `isometry_singleton`, `isAtom_iff`, `continuous_singleton`, `isUniformEmbedding_singleton`, `isClosedEmbedding_singleton`, `TopologicalSpace.NonemptyCompacts.toCloseds_singleton`, `isEmbedding_singleton`, `uniformContinuous_singleton`
`preimage` 📖	CompOp	2 math math: `coe_preimage`, `AlgebraicGeometry.Scheme.IdealSheafData.support_comap`
`singleton` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`carrier_eq_coe` 📖	mathematical	—	`carrier` `SetLike.coe` `TopologicalSpace.Closeds` `instSetLike`	—	—
`closure_le` 📖	mathematical	—	`TopologicalSpace.Closeds` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike`	—	`IsClosed.closure_subset_iff` `isClosed`
`coe_bot` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Closeds` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `Set` `Set.instEmptyCollection`	—	—
`coe_closure` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Closeds` `instSetLike` `closure` `closure`	—	—
`coe_compl` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Opens` `TopologicalSpace.Opens.instSetLike` `compl` `Compl.compl` `Set` `Set.instCompl` `TopologicalSpace.Closeds` `instSetLike`	—	—
`coe_eq_empty` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Closeds` `instSetLike` `Set` `Set.instEmptyCollection` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`SetLike.coe_injective`
`coe_eq_singleton_of_isAtom` 📖	mathematical	`IsAtom` `TopologicalSpace.Closeds` `PartialOrder.toPreorder` `instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `CompleteLattice.toBoundedOrder` `instCompleteLattice`	`SetLike.coe` `instSetLike` `Set` `Set.instSingletonSet`	—	`minimal_nonempty_closed_eq_singleton` `isClosed'` `coe_nonempty` `CanLift.prf` `instCanLiftSetCoeIsClosed` `SetLike.coe_injective` `IsAtom.le_iff_eq`
`coe_eq_univ` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Closeds` `instSetLike` `Set.univ` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`SetLike.coe_injective`
`coe_finset_inf` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Closeds` `instSetLike` `Finset.inf` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `CompleteLattice.toBoundedOrder` `Set` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Set.instOrderTop`	—	`map_finset_inf` `InfTopHom.instInfTopHomClass` `coe_inf` `coe_top`
`coe_finset_sup` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Closeds` `instSetLike` `Finset.sup` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `CompleteLattice.toBoundedOrder` `Set` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`map_finset_sup` `SupBotHom.instSupBotHomClass` `coe_sup` `coe_bot`
`coe_iInf` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Closeds` `instSetLike` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Set.iInter`	—	`Set.ext`
`coe_inf` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Closeds` `instSetLike` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Set` `Set.instInter`	—	—
`coe_mk` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Closeds` `instSetLike`	—	—
`coe_nonempty` 📖	mathematical	—	`Set.Nonempty` `SetLike.coe` `TopologicalSpace.Closeds` `instSetLike`	—	`Set.nonempty_iff_ne_empty` `Iff.not` `coe_eq_empty`
`coe_preimage` 📖	mathematical	`Continuous`	`SetLike.coe` `TopologicalSpace.Closeds` `instSetLike` `preimage` `Set.preimage`	—	—
`coe_sInf` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Closeds` `instSetLike` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Set.iInter` `Set` `Set.instMembership`	—	—
`coe_sSup` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Closeds` `instSetLike` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `closure` `Set.sUnion` `Set.image` `Set`	—	—
`coe_singleton` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Closeds` `instSetLike` `instSingletonOfT1Space` `Set` `Set.instSingletonSet`	—	—
`coe_sup` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Closeds` `instSetLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Set` `Set.instUnion`	—	—
`coe_top` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Closeds` `instSetLike` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `Set.univ`	—	—
`complOrderIso_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `TopologicalSpace.Closeds` `OrderDual` `TopologicalSpace.Opens` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `OrderDual.instLE` `TopologicalSpace.Opens.instPartialOrder` `RelIso.instFunLike` `complOrderIso` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `compl`	—	—
`complOrderIso_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `OrderDual` `TopologicalSpace.Opens` `TopologicalSpace.Closeds` `OrderDual.instLE` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `instPartialOrder` `RelIso.instFunLike` `RelIso.symm` `complOrderIso` `TopologicalSpace.Opens.compl` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual`	—	—
`compl_bijective` 📖	mathematical	—	`Function.Bijective` `TopologicalSpace.Closeds` `TopologicalSpace.Opens` `compl`	—	`Function.bijective_iff_has_inverse` `compl_compl` `TopologicalSpace.Opens.compl_compl`
`compl_compl` 📖	mathematical	—	`TopologicalSpace.Opens.compl` `compl`	—	`ext` `compl_compl`
`ext` 📖	—	`SetLike.coe` `TopologicalSpace.Closeds` `instSetLike`	—	—	`SetLike.ext'`
`ext_iff` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Closeds` `instSetLike`	—	`ext`
`gc` 📖	mathematical	—	`GaloisConnection` `Set` `TopologicalSpace.Closeds` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `instPartialOrder` `closure` `SetLike.coe` `instSetLike`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_closure` `closure_minimal` `isClosed`
`iInf_def` 📖	mathematical	—	`iInf` `TopologicalSpace.Closeds` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Set.iInter` `SetLike.coe` `instSetLike` `isClosed_iInter` `isClosed'`	—	`ext` `isClosed_iInter` `isClosed'` `coe_iInf`
`iInf_mk` 📖	mathematical	`IsClosed`	`iInf` `TopologicalSpace.Closeds` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Set.iInter` `isClosed_iInter`	—	`iInf_def`
`instCanLiftSetCoeIsClosed` 📖	mathematical	—	`CanLift` `Set` `TopologicalSpace.Closeds` `SetLike.coe` `instSetLike` `IsClosed`	—	—
`isAtom_coe` 📖	mathematical	—	`IsAtom` `Set` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `TopologicalSpace.Closeds` `instSetLike` `instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `CompleteLattice.toBoundedOrder` `instCompleteLattice`	—	`GaloisInsertion.isAtom_iff'` `IsAtomistic.instIsAtomic` `Set.instIsAtomistic` `Set.isAtom_iff` `closure_singleton`
`isAtom_iff` 📖	mathematical	—	`IsAtom` `TopologicalSpace.Closeds` `PartialOrder.toPreorder` `instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `CompleteLattice.toBoundedOrder` `instCompleteLattice` `instSingletonOfT1Space`	—	—
`isClosed` 📖	mathematical	—	`IsClosed` `SetLike.coe` `TopologicalSpace.Closeds` `instSetLike`	—	`isClosed'`
`isClosed'` 📖	mathematical	—	`IsClosed` `carrier`	—	—
`mem_closure` 📖	mathematical	—	`TopologicalSpace.Closeds` `SetLike.instMembership` `instSetLike` `closure` `Set` `Set.instMembership` `closure`	—	—
`mem_iInf` 📖	mathematical	—	`TopologicalSpace.Closeds` `SetLike.instMembership` `instSetLike` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	—
`mem_mk` 📖	mathematical	—	`TopologicalSpace.Closeds` `SetLike.instMembership` `instSetLike` `Set` `Set.instMembership`	—	—
`mem_sInf` 📖	mathematical	—	`TopologicalSpace.Closeds` `SetLike.instMembership` `instSetLike` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`Set.mem_iInter₂`
`mem_singleton` 📖	mathematical	—	`TopologicalSpace.Closeds` `SetLike.instMembership` `instSetLike` `instSingletonOfT1Space`	—	—
`mk_singleton` 📖	mathematical	—	`Set` `Set.instSingletonSet` `isClosed_singleton` `TopologicalSpace.Closeds` `instSingletonOfT1Space`	—	`isClosed_singleton`
`singleton_inj` 📖	mathematical	—	`TopologicalSpace.Closeds` `instSingletonOfT1Space`	—	`singleton_injective`
`singleton_injective` 📖	mathematical	—	`TopologicalSpace.Closeds` `instSingletonOfT1Space`	—	`Function.Injective.of_comp` `Set.singleton_injective`

TopologicalSpace.IrreducibleCloseds

Definitions

Name	Category	Theorems
`carrier` 📖	CompOp	4 math math: `isIrreducible'`, `equivSubtype_apply`, `isClosed'`, `equivSubtype'_apply`
`equivSubtype` 📖	CompOp	2 math math: `equivSubtype_apply`, `equivSubtype_symm_apply`
`equivSubtype'` 📖	CompOp	2 math math: `equivSubtype'_apply`, `equivSubtype'_symm_apply`
`instPartialOrder` 📖	CompOp	2 math math: `map_strictMono_of_isInducing`, `map_mono`
`instSetLike` 📖	CompOp	10 math math: `coe_mk`, `instCanLiftSetCoeAndIsIrreducibleIsClosed`, `is_irreducible'`, `isIrreducible`, `isClosed`, `is_closed'`, `coe_singleton`, `mem_singleton`, `ext_iff`, `coe_map`
`instSingletonOfT1Space` 📖	CompOp	5 math math: `singleton_inj`, `singleton_injective`, `coe_singleton`, `mem_singleton`, `mk_singleton`
`map` 📖	CompOp	4 math math: `map_strictMono_of_isInducing`, `map_injective_of_isInducing`, `map_mono`, `coe_map`
`orderIsoSubtype` 📖	CompOp	—
`orderIsoSubtype'` 📖	CompOp	—
`singleton` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_map` 📖	mathematical	`Continuous`	`SetLike.coe` `TopologicalSpace.IrreducibleCloseds` `instSetLike` `map` `closure` `Set.image`	—	—
`coe_mk` 📖	mathematical	`IsIrreducible`	`SetLike.coe` `TopologicalSpace.IrreducibleCloseds` `instSetLike`	—	—
`coe_singleton` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.IrreducibleCloseds` `instSetLike` `instSingletonOfT1Space` `Set` `Set.instSingletonSet`	—	—
`equivSubtype'_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `TopologicalSpace.IrreducibleCloseds` `Set` `IsClosed` `IsIrreducible` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivSubtype'` `carrier`	—	—
`equivSubtype'_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Set` `IsClosed` `IsIrreducible` `TopologicalSpace.IrreducibleCloseds` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivSubtype'`	—	—
`equivSubtype_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `TopologicalSpace.IrreducibleCloseds` `Set` `IsIrreducible` `IsClosed` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivSubtype` `carrier`	—	—
`equivSubtype_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Set` `IsIrreducible` `IsClosed` `TopologicalSpace.IrreducibleCloseds` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivSubtype`	—	—
`ext` 📖	—	`SetLike.coe` `TopologicalSpace.IrreducibleCloseds` `instSetLike`	—	—	`SetLike.ext'`
`ext_iff` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.IrreducibleCloseds` `instSetLike`	—	`ext`
`instCanLiftSetCoeAndIsIrreducibleIsClosed` 📖	mathematical	—	`CanLift` `Set` `TopologicalSpace.IrreducibleCloseds` `SetLike.coe` `instSetLike` `IsIrreducible` `IsClosed`	—	—
`isClosed` 📖	mathematical	—	`IsClosed` `SetLike.coe` `TopologicalSpace.IrreducibleCloseds` `instSetLike`	—	`isClosed'`
`isClosed'` 📖	mathematical	—	`IsClosed` `carrier`	—	—
`isIrreducible` 📖	mathematical	—	`IsIrreducible` `SetLike.coe` `TopologicalSpace.IrreducibleCloseds` `instSetLike`	—	`isIrreducible'`
`isIrreducible'` 📖	mathematical	—	`IsIrreducible` `carrier`	—	—
`is_closed'` 📖	mathematical	—	`IsClosed` `SetLike.coe` `TopologicalSpace.IrreducibleCloseds` `instSetLike`	—	`isClosed`
`is_irreducible'` 📖	mathematical	—	`IsIrreducible` `SetLike.coe` `TopologicalSpace.IrreducibleCloseds` `instSetLike`	—	`isIrreducible`
`map_injective_of_isInducing` 📖	mathematical	`Topology.IsInducing`	`TopologicalSpace.IrreducibleCloseds` `map` `Topology.IsInducing.continuous`	—	`Topology.IsInducing.continuous` `SetLike.coe_injective` `IsClosed.closure_eq` `isClosed` `Topology.IsInducing.closure_eq_preimage_closure_image`
`map_mono` 📖	mathematical	`Continuous`	`Monotone` `TopologicalSpace.IrreducibleCloseds` `PartialOrder.toPreorder` `instPartialOrder` `map`	—	`closure_mono` `Set.image_mono`
`map_strictMono_of_isInducing` 📖	mathematical	`Topology.IsInducing`	`StrictMono` `TopologicalSpace.IrreducibleCloseds` `PartialOrder.toPreorder` `instPartialOrder` `map` `Topology.IsInducing.continuous`	—	`Monotone.strictMono_of_injective` `Topology.IsInducing.continuous` `map_mono` `map_injective_of_isInducing`
`mem_singleton` 📖	mathematical	—	`TopologicalSpace.IrreducibleCloseds` `SetLike.instMembership` `instSetLike` `instSingletonOfT1Space`	—	—
`mk_singleton` 📖	mathematical	—	`Set` `Set.instSingletonSet` `isIrreducible_singleton` `isClosed_singleton` `TopologicalSpace.IrreducibleCloseds` `instSingletonOfT1Space`	—	`isIrreducible_singleton` `isClosed_singleton`
`singleton_inj` 📖	mathematical	—	`TopologicalSpace.IrreducibleCloseds` `instSingletonOfT1Space`	—	`singleton_injective`
`singleton_injective` 📖	mathematical	—	`TopologicalSpace.IrreducibleCloseds` `instSingletonOfT1Space`	—	`Function.Injective.of_comp` `Set.singleton_injective`

TopologicalSpace.Opens

Definitions

Name	Category	Theorems
`compl` 📖	CompOp	6 math math: `TopologicalSpace.Closeds.complOrderIso_symm_apply`, `complOrderIso_apply`, `TopologicalSpace.Closeds.compl_compl`, `compl_bijective`, `coe_compl`, `compl_compl`
`complOrderIso` 📖	CompOp	2 math math: `complOrderIso_apply`, `complOrderIso_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_compl` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Closeds` `TopologicalSpace.Closeds.instSetLike` `compl` `Compl.compl` `Set` `Set.instCompl` `TopologicalSpace.Opens` `instSetLike`	—	—
`complOrderIso_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `TopologicalSpace.Opens` `OrderDual` `TopologicalSpace.Closeds` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `OrderDual.instLE` `TopologicalSpace.Closeds.instPartialOrder` `RelIso.instFunLike` `complOrderIso` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `compl`	—	—
`complOrderIso_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `OrderDual` `TopologicalSpace.Closeds` `TopologicalSpace.Opens` `OrderDual.instLE` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.Closeds.instPartialOrder` `instPartialOrder` `RelIso.instFunLike` `RelIso.symm` `complOrderIso` `TopologicalSpace.Closeds.compl` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual`	—	—
`compl_bijective` 📖	mathematical	—	`Function.Bijective` `TopologicalSpace.Opens` `TopologicalSpace.Closeds` `compl`	—	`Function.bijective_iff_has_inverse` `compl_compl` `TopologicalSpace.Closeds.compl_compl`
`compl_compl` 📖	mathematical	—	`TopologicalSpace.Closeds.compl` `compl`	—	`ext` `compl_compl`
`isCoatom_iff` 📖	mathematical	—	`IsCoatom` `TopologicalSpace.Opens` `PartialOrder.toPreorder` `instPartialOrder` `BoundedOrder.toOrderTop` `Preorder.toLE` `CompleteLattice.toBoundedOrder` `instCompleteLattice` `TopologicalSpace.Closeds.compl` `TopologicalSpace.Closeds` `TopologicalSpace.Closeds.instSingletonOfT1Space`	—	`compl_compl` `isAtom_dual_iff_isCoatom` `OrderIso.isAtom_iff` `Function.Bijective.injective` `TopologicalSpace.Closeds.compl_bijective`

---

← Back to Index