Order

📁 Source: Mathlib/Topology/Order.lean

Statistics

Metric	Count
Definitions DiscreteTopology, IndiscreteTopology, NontrivialTopology, uniqueTopologicalSpace, GenerateOpen, gciGenerateFrom, generateFrom, instCompleteLattice, instPartialOrder, mkOfClosure, mkOfNhds, inhabitedTopologicalSpace, instTopologicalSpaceBool, instTopologicalSpaceEmpty, instTopologicalSpaceFin, instTopologicalSpaceInt, instTopologicalSpaceNat, instTopologicalSpacePEmpty, instTopologicalSpacePUnit, nhdsAdjoint, sierpinskiSpace	21
Theorems coinduced_le, le_induced, eq_bot, of_continuous_injective, of_finite_of_isClosed_singleton, coinduced_symm, induced_symm, eq_top, isOpen_iff, nhds_eq, of_forall_inseparable, all, cast_continuous, mono, mono, cast_continuous, exists_not_inseparable, ne_top, of_exists_not_inseparable, discreteTopology, eq_top_iff_forall_inseparable, gc_generateFrom, generateFrom_anti, generateFrom_setOf_isOpen, generateFrom_surjective, indiscrete_iff_forall_inseparable, indiscrete_or_nontrivial, isOpen_generateFrom_of_mem, isOpen_top_iff, le_def, le_generateFrom_iff_subset_isOpen, leftInverse_generateFrom, mkOfClosure_sets, ne_top_iff_exists_not_inseparable, nhds_generateFrom, nhds_mkOfNhds, nhds_mkOfNhds_filterBasis, nhds_mkOfNhds_of_hasBasis, nhds_mkOfNhds_single, nontrivial_iff_exists_not_inseparable, not_indiscrete_iff, not_nontrivial_iff, setOf_isOpen_injective, tendsto_nhds_generateFrom_iff, mono, closure_discrete, closure_induced, coinduced_bot, coinduced_compose, coinduced_iSup, coinduced_id, coinduced_le_iff_le_induced, coinduced_mono, coinduced_nhdsAdjoint, coinduced_sSup, coinduced_sup, continuous_Prop, continuous_bot, continuous_coinduced_dom, continuous_coinduced_rng, continuous_discrete_rng, continuous_empty_function, continuous_generateFrom_iff, continuous_iInf_dom, continuous_iInf_rng, continuous_iSup_dom, continuous_iSup_rng, continuous_id_iff_le, continuous_id_of_le, continuous_iff_coinduced_le, continuous_iff_le_induced, continuous_induced_dom, continuous_induced_rng, continuous_inf_dom_left, continuous_inf_dom_right, continuous_inf_rng, continuous_le_dom, continuous_le_rng, continuous_nhdsAdjoint_dom, continuous_of_discreteTopology, continuous_sInf_dom, continuous_sInf_rng, continuous_sSup_dom, continuous_sSup_rng, continuous_sup_dom, continuous_sup_rng_left, continuous_sup_rng_right, continuous_top, denseRange_discrete, dense_discrete, discreteTopology_bot, discreteTopology_iff_forall_isClosed, discreteTopology_iff_forall_isOpen, discreteTopology_iff_isOpen_singleton, discreteTopology_iff_nhds, discreteTopology_iff_nhds_ne, discreteTopology_iff_singleton_mem_nhds, eq_bot_of_singletons_open, forall_open_iff_discrete, gc_coinduced_induced, gc_nhds, generateFrom_iInter, generateFrom_iInter_of_generateFrom_eq_self, generateFrom_iUnion, generateFrom_iUnion_isOpen, generateFrom_insert_empty, generateFrom_insert_of_generateOpen, generateFrom_insert_univ, generateFrom_inter, generateFrom_sUnion, generateFrom_union, generateFrom_union_isOpen, indiscreteTopology_iff, induced_compose, induced_const, induced_generateFrom_eq, induced_iInf, induced_id, induced_iff_nhds_eq, induced_inf, induced_mono, induced_sInf, induced_top, inseparable_top, instDiscreteTopologyBool, instDiscreteTopologyEmpty, instDiscreteTopologyFin, instDiscreteTopologyInt, instDiscreteTopologyNat, instDiscreteTopologyPEmpty, instDiscreteTopologyPUnit, instIndiscreteTopology, instIndiscreteTopologyEmpty, instIndiscreteTopologyOfSubsingleton, instIndiscreteTopologyPEmpty, instIndiscreteTopologyPUnit, isClosed_coinduced, isClosed_discrete, isClosed_iSup_iff, isClosed_induced, isClosed_induced_iff, isClosed_induced_iff', isClosed_sSup_iff, isOpen_coinduced, isOpen_discrete, isOpen_iSup_iff, isOpen_iff_continuous_mem, isOpen_implies_isOpen_iff, isOpen_induced, isOpen_induced_eq, isOpen_induced_iff, isOpen_sSup_iff, isOpen_singleton_nhdsAdjoint, isOpen_singleton_true, isOpen_sup, le_generateFrom, le_iff_nhds, le_induced_generateFrom, le_nhdsAdjoint_iff, le_nhdsAdjoint_iff', le_of_nhds_le_nhds, map_nhds_induced_eq, map_nhds_induced_of_mem, map_nhds_induced_of_surjective, mem_nhds_discrete, mem_nhds_induced, nhds_discrete, nhds_false, nhds_iInf, nhds_induced, nhds_inf, nhds_mono, nhds_nhdsAdjoint, nhds_nhdsAdjoint_of_ne, nhds_nhdsAdjoint_same, nhds_sInf, nhds_top, nhds_true, nontrivialTopology_iff, preimage_nhds_coinduced, setOf_isOpen_iSup, setOf_isOpen_sSup, setOf_isOpen_sup, singletons_open_iff_discrete, tendsto_nhds_Prop, tendsto_nhds_true	186
Total	207

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coinduced_le 📖	mathematical	Continuous	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder TopologicalSpace.coinduced	—	continuous_def
le_induced 📖	mathematical	Continuous	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder TopologicalSpace.induced	—	coinduced_le_iff_le_induced coinduced_le

DiscreteTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_bot 📖	mathematical	—	Bot.bot TopologicalSpace OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	—
of_continuous_injective 📖	mathematical	Continuous	DiscreteTopology	—	discreteTopology_iff_forall_isOpen IsOpen.preimage isOpen_discrete Function.Injective.preimage_image
of_finite_of_isClosed_singleton 📖	mathematical	IsClosed Set Set.instSingletonSet	DiscreteTopology	—	discreteTopology_iff_forall_isClosed isClosed_iUnion_of_finite Subtype.finite Set.iUnion_of_singleton_coe

Equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coinduced_symm 📖	mathematical	—	TopologicalSpace.coinduced DFunLike.coe Equiv EquivLike.toFunLike instEquivLike symm TopologicalSpace.induced	—	induced_symm
induced_symm 📖	mathematical	—	TopologicalSpace.induced DFunLike.coe Equiv EquivLike.toFunLike instEquivLike symm TopologicalSpace.coinduced	—	TopologicalSpace.ext isOpen_induced_iff isOpen_coinduced preimage_eq_iff_eq_image image_symm_eq_preimage

IndiscreteTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_top 📖	mathematical	—	Top.top TopologicalSpace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—
isOpen_iff 📖	mathematical	—	IsOpen Set Set.instEmptyCollection Set.univ	—	eq_top Set.inter_self Set.inter_univ Set.inter_empty Set.sUnion_mem_empty_univ isOpen_empty isOpen_univ
nhds_eq 📖	mathematical	—	nhds Top.top Filter Filter.instTop	—	eq_top nhds_top
of_forall_inseparable 📖	mathematical	Inseparable	IndiscreteTopology	—	TopologicalSpace.ext_nhds top_unique mem_of_mem_nhds nhds_top

Inseparable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
all 📖	mathematical	—	Inseparable	—	IndiscreteTopology.nhds_eq

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_continuous 📖	mathematical	—	Continuous instTopologicalSpaceInt	—	continuous_of_discreteTopology instDiscreteTopologyInt

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mono 📖	mathematical	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder	IsClosed	—	isOpen_compl_iff IsOpen.mono isOpen_compl

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mono 📖	—	IsOpen TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder	—	—	—

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_continuous 📖	mathematical	—	Continuous instTopologicalSpaceNat	—	continuous_of_discreteTopology instDiscreteTopologyNat

NontrivialTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_not_inseparable 📖	mathematical	—	Inseparable	—	TopologicalSpace.nontrivial_iff_exists_not_inseparable
ne_top 📖	—	—	—	—	—
of_exists_not_inseparable 📖	mathematical	Inseparable	NontrivialTopology	—	TopologicalSpace.nontrivial_iff_exists_not_inseparable

Subsingleton

Definitions

Name	Category	Theorems
uniqueTopologicalSpace 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
discreteTopology 📖	mathematical	—	DiscreteTopology	—	Unique.eq_default

TopologicalSpace

Definitions

Name	Category	Theorems
GenerateOpen 📖	CompData	3 math math: Topology.IsUpper.isOpen_iff_generate_Iic_compl, Topology.IsLower.isOpen_iff_generate_Ici_compl, isOpen_iff_generate_intervals
gciGenerateFrom 📖	CompOp	—
generateFrom 📖	CompOp	41 math math: generateFrom_insert_of_generateOpen, SecondCountableTopology.mk', tendsto_nhds_generateFrom_iff, generateFrom_sUnion, generateFrom_iUnion_isOpen, generateFrom_union, generateFrom_insert_empty, generateFrom_surjective, ContinuousMap.compactOpen_eq, generateFrom_anti, prod_eq_generateFrom, generateFrom_setOf_isOpen, nhds_generateFrom, le_induced_generateFrom, isOpen_generateFrom_of_mem, generateFrom_iUnion, generateFrom_iInter, pi_eq_generateFrom, continuousOn_isOpen_of_generateFrom, generateFrom_insert_univ, pi_generateFrom_eq, induced_generateFrom_eq, IsTopologicalBasis.eq_generateFrom, gc_generateFrom, LinearOrder.bot_topologicalSpace_eq_generateFrom, prod_generateFrom_generateFrom_eq, exists_countable_generateFrom_Ioi_Iio, generateFrom_union_isOpen, SecondCountableTopology.is_open_generated_countable, OrderTopology.topology_eq_generate_intervals, continuousOn_to_generateFrom_iff, continuous_generateFrom_iff, eq_generateFrom_countableBasis, generateFrom_inter, leftInverse_generateFrom, Dense.topology_eq_generateFrom, ContinuousMap.compactOpen_eq_generateFrom, le_generateFrom_iff_subset_isOpen, le_generateFrom, mkOfClosure_sets, pi_generateFrom_eq_finite
instCompleteLattice 📖	CompOp	159 math math: continuousNeg_iInf, coinduced_bot, continuous_sInf_dom₂, PolynormableSpace.sInf, continuous_sup_rng_right, GroupTopology.toTopologicalSpace_iInf, equicontinuousWithinAt_iInf_dom, continuousMul_inf, ContinuousMap.compactOpen_eq_iInf_induced, nhds_sInf, continuousMul_sInf, AddGroupTopology.toTopologicalSpace_inf, setOf_isOpen_iSup, isClosed_iSup_iff, topologicalGroup_iInf, continuous_sup_dom, R1Space.iInf, nhds_iInf, continuous_sSup_dom, isClosed_sSup_iff, induced_inf, inseparable_top, GroupTopology.toTopologicalSpace_inf, eq_induced_by_maps_to_sierpinski, LocallyConvexSpace.inf, continuousVAdd_sInf, generateFrom_sUnion, continuous_inf_dom_left₂, induced_const, generateFrom_iUnion_isOpen, continuousAdd_inf, eq_top_iff_forall_inseparable, continuous_inf_dom_right₂, UniformSpace.toTopologicalSpace_top, generateFrom_union, isOpen_sup, AddGroupTopology.toTopologicalSpace_sInf, TopCat.pullback_topology, generateFrom_iInter_of_generateFrom_eq_self, TopCat.colimit_topology, topologicalGroup_inf, Pi.induced_restrict, topologicalAddGroup_inf, induced_topology_pure, continuousNeg_sInf, continuous_sSup_rng, continuousNeg_inf, TopCat.prod_topology, IndiscreteTopology.eq_top, regularSpace_sInf, topologicalAddGroup_sInf, isOpen_top_iff, IsTopologicalBasis.inf_induced, continuous_iInf_rng, continuous_bot, continuousInv_inf, continuous_inf_dom_right, isOpen_sSup_iff, isDenseEmbedding_pure, induced_sInf, TopCat.nonempty_isLimit_iff_eq_induced, SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf, CompletePseudometrizable.iInf, SequentialSpace.iSup, continuousInv_sInf, continuous_top, pullbackTopology_def, secondCountableTopology_iInf, AddGroupTopology.toTopologicalSpace_top, LocallyConvexSpace.iInf, Topology.IsGeneratedBy.sup, continuousSMul_sInf, generateFrom_iUnion, coinduced_sSup, LinearMap.mem_span_iff_continuous_of_finite, nhds_top, UniformOnFun.topologicalSpace_eq, IsTopologicalBasis.inf, GroupTopology.toTopologicalSpace_sInf, continuousAdd_iInf, regularSpace_iInf, continuous_iSup_dom, R1Space.inf, equicontinuous_iInf_dom, UniformSpace.toTopologicalSpace_bot, CompHausLike.LocallyConstant.locallyConstantIsoContinuousMap_hom, generateFrom_iInter, alexandrovDiscrete_iSup, continuous_sInf_dom, UniformSpace.toTopologicalSpace_sInf, GroupTopology.toTopologicalSpace_bot, PolynormableSpace.iInf, nhds_inf, TopCat.coinduced_of_isColimit, topologicalGroup_sInf, isOpen_iSup_iff, AlexandrovDiscrete.sup, Pi.induced_precomp, UniformSpace.toTopologicalSpace_iInf, indiscreteTopology_iff, continuousSMul_inf, continuousAdd_sInf, DeltaGeneratedSpace.sup, LocallyConvexSpace.sInf, RegularSpace.inf, Units.topology_eq_inf, completelyRegularSpace_iInf, continuousSMul_iInf, coinduced_iSup, IsTopologicalBasis.iInf, Pi.induced_restrict_sUnion, discreteTopology_bot, equicontinuousAt_iInf_dom, completelyRegularSpace_inf, isDenseInducing_pure, continuous_iSup_rng, induced_to_pi, continuousMul_iInf, TopCat.induced_of_isLimit, continuous_iInf_dom, continuousVAdd_inf, coinduced_sup, LinearOrder.bot_topologicalSpace_eq_generateFrom, inducing_iInf_to_pi, TopCat.nonempty_isColimit_iff_eq_coinduced, DiscreteTopology.eq_bot, equicontinuousOn_iInf_dom, generateFrom_union_isOpen, UniformSpace.toTopologicalSpace_inf, eq_bot_of_singletons_open, Pi.induced_precomp', continuousInv_iInf, RestrictedProduct.topologicalSpace_eq_iSup, withSeminorms_iInf, continuous_sup_rng_left, induced_top, setOf_isOpen_sSup, continuous_inf_rng, GroupTopology.toTopologicalSpace_top, AddGroupTopology.toTopologicalSpace_iInf, Topology.IsGeneratedBy.iSup, PolishSpace.iInf, induced_iInf, TopCat.limit_topology, generateFrom_inter, R1Space.sInf, PolynormableSpace.inf, SequentialSpace.sup, instIndiscreteTopology, LinearMap.mem_span_iff_continuous, AddUnits.topology_eq_inf, topologicalAddGroup_iInf, DeltaGeneratedSpace.iSup, continuous_inf_dom_left, continuous_sInf_rng, continuousVAdd_iInf, IsTopologicalBasis.iInf_induced, AddGroupTopology.toTopologicalSpace_bot, setOf_isOpen_sup
instPartialOrder 📖	CompOp	54 math math: Topology.lawson_le_scott, le_nhdsAdjoint_iff, Topology.IsGeneratedBy.le_generatedBy, UCompactlyGeneratedSpace.le_compactlyGenerated, deltaGenerated_le, le_of_nhds_le_nhds, t2Space_antitone, UniformConvergenceCLM.topologicalSpace_mono, Measurable.exists_continuous, Topology.upperSet_le_scott, le_def, Topology.IsGeneratedBy.iff_le_generatedBy, generateFrom_anti, Topology.isLawson_le_isScott, le_nhdsAdjoint_iff', le_induced_generateFrom, Topology.scottHausdorff_le_isLawson, t1Space_antitone, DeltaGeneratedSpace.le_deltaGenerated, Topology.scottHausdorff_le_lawson, continuous_iff_le_induced, coinduced_le_iff_le_induced, Topology.IsScott.scottHausdorff_le, Topology.scottHausdorff_le_scott, AddGroupTopology.toTopologicalSpace_le, Topology.scottHausdorff_le_lower, continuous_id_iff_le, induced_topology_le_preorder, le_iff_nhds, Continuous.le_induced, NormedSpace.Dual.dual_norm_topology_le_weak_dual_topology, generatedBy_le, moduleTopology_le, isOpen_implies_isOpen_iff, gc_generateFrom, GroupTopology.toTopologicalSpace_le, gc_nhds, Topology.IsUpperSet.upperSet_le_upper, MeasureTheory.LevyProkhorov.le_convergenceInDistribution, continuous_iff_coinduced_le, MeasureTheory.levyProkhorov_le_convergenceInDistribution, Topology.lawson_le_lower, borel_anti, ContinuousMap.compactOpen_le_induced, UniformSpace.toTopologicalSpace_mono, Topology.IsLower.scottHausdorff_le, TestFunction.topologicalSpace_le_iff, Topology.IsLowerSet.lowerSet_le_lower, gc_coinduced_induced, le_generateFrom_iff_subset_isOpen, le_generateFrom, Opens.IsBasis.le_iff, TestFunction.originalTop_le, Continuous.coinduced_le
mkOfClosure 📖	CompOp	1 math math: mkOfClosure_sets
mkOfNhds 📖	CompOp	4 math math: nhds_mkOfNhds_single, nhds_mkOfNhds_of_hasBasis, nhds_mkOfNhds_filterBasis, nhds_mkOfNhds

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_top_iff_forall_inseparable 📖	mathematical	—	Top.top TopologicalSpace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Inseparable	—	indiscrete_iff_forall_inseparable indiscreteTopology_iff
gc_generateFrom 📖	mathematical	—	GaloisConnection TopologicalSpace OrderDual Set PartialOrder.toPreorder instPartialOrder OrderDual.instPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual setOf IsOpen generateFrom OrderDual.ofDual	—	le_generateFrom_iff_subset_isOpen
generateFrom_anti 📖	mathematical	Set Set.instHasSubset	TopologicalSpace Preorder.toLE PartialOrder.toPreorder instPartialOrder generateFrom	—	GaloisConnection.monotone_u gc_generateFrom
generateFrom_setOf_isOpen 📖	mathematical	—	generateFrom setOf Set IsOpen	—	GaloisCoinsertion.u_l_eq
generateFrom_surjective 📖	mathematical	—	Set TopologicalSpace generateFrom	—	GaloisCoinsertion.u_surjective
indiscrete_iff_forall_inseparable 📖	mathematical	—	IndiscreteTopology Inseparable	—	Inseparable.all IndiscreteTopology.of_forall_inseparable
indiscrete_or_nontrivial 📖	mathematical	—	IndiscreteTopology NontrivialTopology	—	eq_or_ne
isOpen_generateFrom_of_mem 📖	mathematical	Set Set.instMembership	IsOpen generateFrom	—	—
isOpen_top_iff 📖	mathematical	—	IsOpen Top.top TopologicalSpace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Set Set.instEmptyCollection Set.univ	—	IndiscreteTopology.isOpen_iff instIndiscreteTopology
le_def 📖	mathematical	—	TopologicalSpace Preorder.toLE PartialOrder.toPreorder instPartialOrder Pi.hasLe Set Prop.le IsOpen	—	—
le_generateFrom_iff_subset_isOpen 📖	mathematical	—	TopologicalSpace Preorder.toLE PartialOrder.toPreorder instPartialOrder generateFrom Set Set.instHasSubset setOf IsOpen	—	isOpen_univ IsOpen.inter isOpen_sUnion
leftInverse_generateFrom 📖	mathematical	—	TopologicalSpace Set generateFrom setOf IsOpen	—	GaloisCoinsertion.u_l_leftInverse
mkOfClosure_sets 📖	mathematical	setOf Set GenerateOpen	mkOfClosure generateFrom	—	ext
ne_top_iff_exists_not_inseparable 📖	mathematical	—	Inseparable	—	nontrivial_iff_exists_not_inseparable nontrivialTopology_iff
nhds_generateFrom 📖	mathematical	—	nhds generateFrom iInf Filter Set Filter.instInfSet Set.instMembership setOf Filter.principal	—	nhds_def le_antisymm biInf_mono le_iInf₂ iInf₂_le LE.le.trans_eq le_top Filter.principal_univ le_inf Filter.inf_principal LE.le.trans Filter.principal_mono Set.subset_sUnion_of_mem
nhds_mkOfNhds 📖	mathematical	Pi.hasLe Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.instPure Filter.Eventually Set Filter.instMembership	nhds mkOfNhds	—	nhds_mkOfNhds_of_hasBasis Filter.basis_sets
nhds_mkOfNhds_filterBasis 📖	mathematical	Set Set.instMembership FilterBasis instMembershipSetFilterBasis Set.instHasSubset	nhds mkOfNhds FilterBasis.filter	—	nhds_mkOfNhds_of_hasBasis FilterBasis.hasBasis
nhds_mkOfNhds_of_hasBasis 📖	mathematical	Filter.HasBasis Set Set.instMembership Filter.Eventually Filter Filter.instMembership	nhds mkOfNhds	—	le_antisymm Filter.HasBasis.ge_iff mem_nhds_iff Filter.HasBasis.mem_iff Filter.Eventually.mono Filter.mem_of_superset nhds_basis_opens
nhds_mkOfNhds_single 📖	mathematical	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.instPure	nhds mkOfNhds Function.update	—	nhds_mkOfNhds le_update_iff le_rfl eq_or_ne Filter.mp_mem Filter.univ_mem' Function.update_of_ne
nontrivial_iff_exists_not_inseparable 📖	mathematical	—	NontrivialTopology Inseparable	—	Iff.not indiscrete_iff_forall_inseparable
not_indiscrete_iff 📖	mathematical	—	IndiscreteTopology NontrivialTopology	—	NontrivialTopology.ne_top IndiscreteTopology.eq_top
not_nontrivial_iff 📖	mathematical	—	NontrivialTopology IndiscreteTopology	—	Iff.not_right not_indiscrete_iff
setOf_isOpen_injective 📖	mathematical	—	TopologicalSpace Set setOf IsOpen	—	GaloisCoinsertion.l_injective
tendsto_nhds_generateFrom_iff 📖	mathematical	—	Filter.Tendsto nhds generateFrom Set Filter Filter.instMembership Set.preimage	—	nhds_generateFrom forall_swap

(root)

Definitions

Name	Category	Theorems
DiscreteTopology 📖	CompData	142 math math: DiscreteContAction.instDiscreteTopologyCarrierObjTopCatForget₂ContinuousMap, discreteTopology_iff_locallyInjective, IsDiscrete.to_subtype, discreteTopology_of_isOpen_singleton_zero, PrimeSpectrum.discreteTopology_iff_finite_and_krullDimLE_zero, QuotientGroup.discreteTopology, discreteTopology_subtype_iff', instDiscreteTopologyProd, PrimeSpectrum.discreteTopology_iff_finite_isMaximal_and_sInf_le_nilradical, PrimeSpectrum.instDiscreteTopology, instDiscreteTopologyULift, AddSubgroup.discreteTopology_iff_of_isFiniteRelIndex, ZLattice.comap_discreteTopology, compl_mem_codiscrete_iff, NormedField.discreteTopology_or_nontriviallyNormedField, Subgroup.instDiscreteTopologyQuotientOfContinuousMul, instDiscreteTopologyMatrixOfFinite, instDiscreteTopologyFin, is_bot_adic_iff, discreteTopology_of_isOpen_singleton_one, DiscreteTopology.of_forall_le_norm, discreteTopology_of_noAccPts, Subgroup.discreteTopology, instDiscreteTopologyPUnit, PrimeSpectrum.discreteTopology_of_toLocalization_surjective, instDiscreteTopologyBool, CategoryTheory.PreGaloisCategory.obj_discreteTopology, Units.instDiscreteTopology, NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIdealLattice, Matrix.SpecialLinearGroup.instDiscreteTopology, JacobsonSpace.discreteTopology, instDiscreteTopologyInt, DiscreteTopology.of_continuous_injective, AlgebraicGeometry.IsLocallyArtinian.iff_isLocallyNoetherian_and_discreteTopology, QuotientAddGroup.discreteTopology_iff, Valued.discreteTopology_of_forall_lt, DiscreteUniformity.instDiscreteTopology, Subgroup.discrete_iff_cyclic, instDiscreteTopologyPEmpty, ChartedSpace.discreteTopology, AddSubgroup.discrete_iff_addCyclic, Homeomorph.discreteTopology_iff, Continuous.discrete_of_tendsto_cofinite_cocompact, forall_open_iff_discrete, AddSubgroup.discreteTopology, isDiscrete_univ_iff, DiscreteTopology.of_predOrder_succOrder, AddSubgroup.discreteTopology_iff_of_finiteIndex, AlgebraicGeometry.IsLocallyArtinian.discreteTopology, ZMod.instDiscreteTopology, FintypeCat.discreteTopology, instDiscreteTopologyAdditive, QuotientGroup.discreteTopology_iff, AddUnits.instDiscreteTopology, PrimeSpectrum.discreteTopology_iff_toPiLocalization_surjective, IsLocalHomeomorph.comap_discreteTopology, CategoryTheory.PreGaloisCategory.aut_discreteTopology, DomAddAct.instDiscreteTopology, Finite.instDiscreteTopology, DomMulAct.instDiscreteTopology, Subgroup.instDiscreteTopStrictPeriods, AlgebraicGeometry.IsArtinianScheme.iff_isNoetherian_and_discreteTopology, instDiscreteTopologyNat, Topology.IsEmbedding.discreteTopology, ZSpan.instDiscreteTopologySubtypeMemSubmoduleIntSpanRangeCoeBasisRealOfFinite, NumberField.Units.instDiscrete_unitLattice, NumberField.mixedEmbedding.euclidean.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, instDiscreteTopologySubtype, AddSubgroup.instDiscreteTopologyQuotientOfContinuousAdd, Subgroup.discreteTopology_iff_of_isFiniteRelIndex, DiscreteQuotient.instDiscreteTopologyQuotient, discreteTopology_iff_singleton_mem_nhds, instDiscreteTopologyOfAlexandrovDiscreteOfT1Space, discreteTopology_bot, discreteTopology_iff_forall_isClosed, TopCat.instDiscreteTopologyCarrierObjDiscrete, Subgroup.discreteTopology_iff_of_finiteIndex, List.instDiscreteTopology, AddSubgroup.instDiscreteTopologyZMultiples, AlgebraicGeometry.IsLocallyArtinian.discreteTopology_of_isAffine, NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, instDiscreteTopologySignType, discreteTopology_subtype_iff, Valued.discreteTopology_of_forall_map_eq_one, PeriodPair.instDiscreteTopologySubtypeComplexMemSubmoduleIntLattice, IsLocalHomeomorphOn.discreteTopology_image_iff, DiscreteTopology.of_finite_of_isClosed_singleton, MulOpposite.instDiscreteTopology, ZSpan.instDiscreteTopologySubtypeMemAddSubgroupToAddSubgroupIntSpanRangeCoeBasisRealOfFinite, discreteTopology_iff_forall_isOpen, discreteTopology_of_discrete_uniformity, DiscreteTopology.of_forall_le_dist, IsLocalHomeomorphOn.discreteTopology_of_image, OrderDual.instDiscreteTopology, NormedField.discreteTopology_of_bddAbove_range_norm, instDiscreteTopologySubtypeMemSubmoduleIntComap, Int.instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples, DiscreteTopology.of_subset, Homeomorph.discreteTopology, FintypeCatDiscrete.instDiscreteTopologyCarrier, Subsingleton.discreteTopology, Algebra.QuasiFinite.discreteTopology_primeSpectrum, isDiscrete_iff_discreteTopology, krullTopology_discreteTopology_of_finiteDimensional, exists_infinite_discreteTopology, IsLocalHomeomorph.discreteTopology_range_iff, AddSubgroup.Commensurable.discreteTopology_iff, discreteTopology_iff_isOpen_singleton, ZSpan.discreteTopology_pi_basisFun, instDiscreteTopologyMultiplicative, AddOpposite.instDiscreteTopology, discreteTopology_union, QuotientAddGroup.discreteTopology, Matrix.SpecialLinearGroup.discreteSpecialLinearGroupIntRange, instDiscreteTopologyZerothHomotopy, DiscreteTopology.preimage_of_continuous_injective, discreteTopology_iff_isOpen_singleton_zero, discreteTopology_iff_nhds_ne, TopologicalSpace.NoetherianSpace.discrete, AddAction.IsPretransitive.discreteTopology_iff, MulAction.IsPretransitive.discreteTopology_iff, SetLike.isDiscrete_iff_discreteTopology, instDiscreteTopologyOfFiniteOfJacobsonSpace, PNat.instDiscreteTopology, IsEvenlyCovered.discreteTopology_fiber, Subgroup.instDiscreteTopologyZMultiples, IsLocalHomeomorph.discreteTopology_iff_of_surjective, Subgroup.instDiscreteTopPeriods, Subgroup.Commensurable.discreteTopology_iff, discreteTopology_iff_isOpen_singleton_one, NormedSpace.discreteTopology_zmultiples, Hamming.instDiscreteTopology, Subgroup.IsArithmetic.discreteTopology, singletons_open_iff_discrete, instDiscreteTopologyConnectedComponentsOfLocallyConnectedSpace, instDiscreteTopologyEmpty, discreteTopology_iff_nhds, instDiscreteTopologySubtypeGeneralLinearGroupMemSubgroupAdjoinNegOneOfIsTopologicalRingOfT2Space, PrimeSpectrum.discreteTopology_iff_toPiLocalization_bijective, discreteTopology_iff_orderTopology_of_pred_succ, DiscreteTopology.of_forall_le_norm', Sum.discreteTopology
IndiscreteTopology 📖	CompData	25 math math: Homeomorph.indiscreteTopology_iff, IndiscreteTopology.of_forall_nnnorm_eq_zero, instIndiscreteTopologyPUnit, indiscreteTopology_iff_forall_norm_eq_zero, IndiscreteTopology.of_forall_inseparable, indiscreteTopology_iff_forall_nnnorm_eq_zero, TopologicalSpace.indiscrete_or_nontrivial, indiscreteTopology_iff_forall_nnnorm_eq_zero', TopologicalSpace.not_indiscrete_iff, indiscreteTopology_iff_forall_norm_eq_zero', TopologicalSpace.not_nontrivial_iff, Topology.IsInducing.indiscreteTopology, SeparationQuotient.inseparableSetoid_eq_top_iff, instIndiscreteTopologyPEmpty, EMetric.subsingleton_iff_indiscreteTopology, IndiscreteTopology.of_forall_nnnorm_eq_zero', instIndiscreteTopologyOfSubsingleton, indiscreteTopology_iff, IndiscreteTopology.of_forall_norm_eq_zero', IndiscreteTopology.of_forall_norm_eq_zero, instIndiscreteTopologyEmpty, TopologicalSpace.indiscrete_iff_forall_inseparable, Homeomorph.indiscreteTopology, SeparationQuotient.subsingleton_iff, instIndiscreteTopology
NontrivialTopology 📖	CompData	20 math math: NontrivialTopology.of_exists_norm_ne_zero', Homeomorph.nontrivialTopology_iff, nontrivialTopology_iff_exists_nnnorm_ne_zero, Topology.IsInducing.nontrivialTopology, TopologicalSpace.indiscrete_or_nontrivial, TopologicalSpace.not_indiscrete_iff, TopologicalSpace.nontrivial_iff_exists_not_inseparable, TopologicalSpace.not_nontrivial_iff, nontrivialTopology_iff_exists_nnnorm_ne_zero', SeparationQuotient.nontrivial_iff, NontrivialTopology.of_exists_norm_ne_zero, nontrivialTopology_iff_exists_norm_ne_zero, Homeomorph.nontrivialTopology, NontrivialTopology.of_exists_nnnorm_ne_zero, EMetric.nontrivial_iff_nontrivialTopology, nontrivialTopology_iff_exists_norm_ne_zero', NontrivialTopology.of_exists_nnnorm_ne_zero', EMetric.instNontrivialTopologyOfNontrivial, nontrivialTopology_iff, NontrivialTopology.of_exists_not_inseparable
inhabitedTopologicalSpace 📖	CompOp	—
instTopologicalSpaceBool 📖	CompOp	77 math math: Profinite.NobelingProof.injective_πs', continuousOn_boolIndicator_iff_isClopen, Profinite.NobelingProof.Products.span_nil_eq_top, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_union_smaller, Profinite.NobelingProof.coe_πs, Profinite.NobelingProof.instSubsingletonLocallyConstantElemForallBoolEmptyCollectionSetInt, Profinite.NobelingProof.Products.max_eq_eval, Profinite.NobelingProof.Products.eval_πs, Profinite.NobelingProof.GoodProducts.injective, Profinite.NobelingProof.GoodProducts.equiv_toFun_eq_eval, Profinite.NobelingProof.Products.eval_πs', Profinite.NobelingProof.GoodProducts.span_sum, Profinite.NobelingProof.GoodProducts.range_equiv_factorization, Profinite.NobelingProof.fin_comap_jointlySurjective, exists_retractionCantorSet, Profinite.NobelingProof.GoodProducts.spanFin, Profinite.NobelingProof.succ_exact, Profinite.NobelingProof.GoodProducts.smaller_factorization, Profinite.NobelingProof.πs'_apply_apply, instDiscreteTopologyBool, Profinite.NobelingProof.Products.eval_eq, Profinite.NobelingProof.Products.evalFacProps, continuous_bool_rng, continuous_isRight, Profinite.NobelingProof.continuous_swapTrue, Profinite.NobelingProof.iso_map_bijective, Profinite.NobelingProof.Products.eval_πs_image', Profinite.NobelingProof.factors_prod_eq_basis_of_ne, Profinite.NobelingProof.continuous_projRestrict, Profinite.NobelingProof.continuous_CC'₁, exists_nat_bool_continuous_surjective_of_compact, Profinite.NobelingProof.GoodProducts.span, Profinite.NobelingProof.isClosed_C0, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_smaller, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_sum, Perfect.exists_nat_bool_injection, Profinite.NobelingProof.e_mem_of_eq_true, Profinite.NobelingProof.πs_apply_apply, Profinite.NobelingProof.GoodProducts.finsuppSum_mem_span_eval, Profinite.NobelingProof.GoodProducts.linearIndependent, Profinite.NobelingProof.GoodProducts.square_commutes, Profinite.NobelingProof.spanFinBasis.span, continuous_boolIndicator_iff_isClopen, Profinite.NobelingProof.isClosed_proj, Profinite.NobelingProof.isClosed_C', IsClosed.exists_nat_bool_injection_of_not_countable, Profinite.NobelingProof.continuous_projRestricts, Profinite.NobelingProof.GoodProducts.smaller_mono, Profinite.NobelingProof.GoodProducts.linearIndependentEmpty, cantorToHilbert_continuous, Profinite.NobelingProof.GoodProducts.span_iff_products, Profinite.NobelingProof.GoodProducts.sum_equiv_comp_eval_eq_elim, Profinite.NobelingProof.CC_comp_zero, Profinite.NobelingProof.eval_eq_πJ, Profinite.NobelingProof.continuous_CC'₀, Profinite.NobelingProof.Products.evalFacProp, Profinite.NobelingProof.Products.evalCons, Profinite.NobelingProof.one_sub_e_mem_of_false, Profinite.NobelingProof.injective_πs, Profinite.Nobeling.isClosedEmbedding, Profinite.NobelingProof.coe_πs', Profinite.NobelingProof.continuous_proj, Profinite.NobelingProof.GoodProducts.range_equiv_smaller_toFun_bijective, continuous_isLeft, Profinite.NobelingProof.list_prod_apply, Bool.borelSpace, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_range, Profinite.NobelingProof.GoodProducts.max_eq_eval, Profinite.NobelingProof.GoodProducts.linearIndependentSingleton, Profinite.NobelingProof.Products.eval_πs_image, Profinite.NobelingProof.isClosed_C1, Real.fromBinary_continuous, Profinite.NobelingProof.factors_prod_eq_basis, Profinite.NobelingProof.factors_prod_eq_basis_of_eq, Profinite.NobelingProof.GoodProducts.union, Profinite.NobelingProof.GoodProducts.max_eq_eval_unapply, Profinite.NobelingProof.succ_mono
instTopologicalSpaceEmpty 📖	CompOp	3 math math: Empty.borelSpace, instIndiscreteTopologyEmpty, instDiscreteTopologyEmpty
instTopologicalSpaceFin 📖	CompOp	3 math math: ContinuousMap.exists_finite_approximation_of_mem_nhds_diagonal, instDiscreteTopologyFin, Real.continuous_ofDigits
instTopologicalSpaceInt 📖	CompOp	15 math math: Int.borelSpace, AddGroup.continuousSMul_int, Int.cast_continuous, continuousAt_toIocDiv, instDiscreteTopologyInt, Int.isClosedEmbedding_coe_real, Matrix.SpecialLinearGroup.isClosedEmbedding_mapGLInt, instNoncompactSpaceInt, continuousWithinAt_toIocDiv_Iic, continuousAt_toIcoDiv, continuousOn_toIocDiv, continuousOn_toIcoDiv, continuousWithinAt_toIcoDiv_Ici, Int.isClosedEmbedding_coe_rat, Complex.closedEmbedding_intCast
instTopologicalSpaceNat 📖	CompOp	22 math math: exists_nat_nat_continuous_surjective_of_completeSpace, LightProfinite.continuous_iff_convergent, AddMonoid.continuousSMul_nat, Nat.instNoncompactSpace, Nat.cast_continuous, LightProfinite.instMetrizableSpaceOnePointNat, Nat.isClosedEmbedding_coe_rat, instDiscreteTopologyNat, PolishSpace.exists_nat_nat_continuous_surjective, TopologicalSpace.exists_isInducing_l_infty, exists_topology_isEmbedding_nat, ENat.isEmbedding_natCast, Nat.isClosedEmbedding_coe_real, PadicInt.mahlerEquiv_apply, TopologicalSpace.exists_embedding_l_infty, MeasureTheory.AnalyticSet_def, PadicInt.mahlerEquiv_symm_apply, List.continuousAt_length, OnePoint.continuous_iff_from_nat, LightProfinite.isClosedEmbedding_natUnionInftyEmbedding, ENat.isOpenEmbedding_natCast, Nat.borelSpace
instTopologicalSpacePEmpty 📖	CompOp	5 math math: AlgebraicGeometry.Scheme.emptyTo_base, instDiscreteTopologyPEmpty, instIndiscreteTopologyPEmpty, AlgebraicGeometry.Scheme.emptyTo_c_app, AlgebraicGeometry.Scheme.empty_presheaf
instTopologicalSpacePUnit 📖	CompOp	47 math math: LightCondensed.isoFinYonedaComponents_hom_apply, condensedSetToTopCat_obj_carrier, LightCondSet.continuous_coinducingCoprod, CompHausLike.LocallyConstant.adjunction_counit, LightCondSet.topCatAdjunctionUnit_val_app_apply, Unit.borelSpace, instIndiscreteTopologyPUnit, CompHausLike.LocallyConstant.counitApp_app, Condensed.isoFinYonedaComponents_hom_apply, CondensedSet.topCatAdjunctionCounit_hom_apply, CompHausLike.LocallyConstant.incl_of_counitAppApp, instDiscreteTopologyPUnit, Path.instSubsingletonPUnitUnit, ContractibleSpace.hequiv_unit, FundamentalGroupoid.instSubsingletonHomPUnit, Homeomorph.prodPUnit_apply, LightCondensed.isoFinYonedaComponents_inv_comp, CondensedSet.topCatAdjunctionUnit_val_app_apply, LightCondensed.isoLocallyConstantOfIsColimit_inv, Condensed.isoLocallyConstantOfIsColimit_inv, CompHausLike.LocallyConstant.adjunction_left_triangle, Condensed.isoFinYonedaComponents_inv_comp, CondensedSet.continuous_coinducingCoprod, TopCat.Presheaf.isSheaf_on_punit_of_isTerminal, skyscraperPresheaf_eq_pushforward, FundamentalGroupoid.punitEquivDiscretePUnit_unitIso, CondensedSet.topCatAdjunctionUnit_val_app, LightCondensed.underlying_obj, ContractibleSpace.hequiv_unit', TopCat.Presheaf.isSheaf_on_punit_iff_isTerminal, lightCondSetToTopCat_obj_carrier, CompHausLike.LocallyConstant.instIsIsoFunctorTypeUnitSheafCoherentTopologyAdjunction, CompHausLike.LocallyConstant.counit_app_val, CompHausLike.LocallyConstant.unit_app, LightCondSet.topCatAdjunctionUnit_val_app, Condensed.underlying_obj, CompHausLike.LocallyConstant.incl_comap, FundamentalGroupoid.punitEquivDiscretePUnit_counitIso, CondensedSet.toTopCatMap_hom_apply, LightCondensed.underlying_map, FundamentalGroupoid.punitEquivDiscretePUnit_inverse, Condensed.underlying_map, LightCondSet.toTopCatMap_hom_apply, Topology.IsGeneratedBy.instPUnit, Homeomorph.coe_punitProd, CompHausLike.LocallyConstant.adjunction_unit, FundamentalGroupoid.punitEquivDiscretePUnit_functor
nhdsAdjoint 📖	CompOp	9 math math: le_nhdsAdjoint_iff, nhds_nhdsAdjoint_of_ne, coinduced_nhdsAdjoint, nhds_nhdsAdjoint, le_nhdsAdjoint_iff', isOpen_singleton_nhdsAdjoint, nhds_nhdsAdjoint_same, gc_nhds, continuous_nhdsAdjoint_dom
sierpinskiSpace 📖	CompOp	15 math math: isOpen_iff_continuous_mem, TopologicalSpace.eq_induced_by_maps_to_sierpinski, nhds_false, nhds_true, tendsto_nhds_Prop, TopologicalSpace.productOfMemOpens_isEmbedding, instIsUpperProp, TopologicalSpace.productOfMemOpens_injective, isOpen_singleton_true, TopologicalSpace.productOfMemOpens_isInducing, instCompletelyNormalSpaceProp, Topology.IsScott.ωScottContinuous_iff_continuous, continuous_Prop, tendsto_nhds_true, Topology.IsUpperSet.instProp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_discrete 📖	mathematical	—	closure	—	IsClosed.closure_eq isClosed_discrete
closure_induced 📖	mathematical	—	Set Set.instMembership closure TopologicalSpace.induced Set.image	—	nhds_induced
coinduced_bot 📖	mathematical	—	TopologicalSpace.coinduced Bot.bot TopologicalSpace OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	GaloisConnection.l_bot gc_coinduced_induced
coinduced_compose 📖	mathematical	—	TopologicalSpace.coinduced	—	TopologicalSpace.ext
coinduced_iSup 📖	mathematical	—	TopologicalSpace.coinduced iSup TopologicalSpace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	GaloisConnection.l_iSup gc_coinduced_induced
coinduced_id 📖	mathematical	—	TopologicalSpace.coinduced	—	TopologicalSpace.ext
coinduced_le_iff_le_induced 📖	mathematical	—	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder TopologicalSpace.coinduced TopologicalSpace.induced	—	—
coinduced_mono 📖	mathematical	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder	TopologicalSpace.coinduced	—	GaloisConnection.monotone_l gc_coinduced_induced
coinduced_nhdsAdjoint 📖	mathematical	—	TopologicalSpace.coinduced nhdsAdjoint Filter.map	—	eq_of_forall_ge_iff gc_nhds continuous_iff_coinduced_le continuous_nhdsAdjoint_dom Filter.Tendsto.eq_1
coinduced_sSup 📖	mathematical	—	TopologicalSpace.coinduced SupSet.sSup TopologicalSpace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice Set.image	—	sSup_eq_iSup' sSup_image' coinduced_iSup
coinduced_sup 📖	mathematical	—	TopologicalSpace.coinduced TopologicalSpace SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	GaloisConnection.l_sup gc_coinduced_induced
continuous_Prop 📖	mathematical	—	Continuous sierpinskiSpace IsOpen setOf	—	—
continuous_bot 📖	mathematical	—	Continuous Bot.bot TopologicalSpace OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	continuous_iff_le_induced bot_le
continuous_coinduced_dom 📖	mathematical	—	Continuous TopologicalSpace.coinduced	—	coinduced_compose
continuous_coinduced_rng 📖	mathematical	—	Continuous TopologicalSpace.coinduced	—	continuous_iff_coinduced_le le_rfl
continuous_discrete_rng 📖	mathematical	—	Continuous IsOpen Set.preimage Set Set.instSingletonSet	—	IsOpen.preimage isOpen_discrete Set.biUnion_of_singleton Set.preimage_iUnion₂ isOpen_biUnion
continuous_empty_function 📖	mathematical	—	Continuous	—	continuous_of_discreteTopology Subsingleton.discreteTopology IsEmpty.instSubsingleton Function.isEmpty
continuous_generateFrom_iff 📖	mathematical	—	Continuous TopologicalSpace.generateFrom IsOpen Set.preimage	—	continuous_iff_coinduced_le TopologicalSpace.le_generateFrom_iff_subset_isOpen
continuous_iInf_dom 📖	mathematical	Continuous	iInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	continuous_le_dom iInf_le
continuous_iInf_rng 📖	mathematical	—	Continuous iInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	—
continuous_iSup_dom 📖	mathematical	—	Continuous iSup TopologicalSpace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	—
continuous_iSup_rng 📖	mathematical	Continuous	iSup TopologicalSpace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	continuous_sSup_rng
continuous_id_iff_le 📖	mathematical	—	Continuous TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder	—	continuous_def
continuous_id_of_le 📖	mathematical	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder	Continuous	—	continuous_id_iff_le
continuous_iff_coinduced_le 📖	mathematical	—	Continuous TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder TopologicalSpace.coinduced	—	continuous_def
continuous_iff_le_induced 📖	mathematical	—	Continuous TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder TopologicalSpace.induced	—	continuous_iff_coinduced_le gc_coinduced_induced
continuous_induced_dom 📖	mathematical	—	Continuous TopologicalSpace.induced	—	continuous_iff_le_induced le_rfl
continuous_induced_rng 📖	mathematical	—	Continuous TopologicalSpace.induced	—	induced_compose
continuous_inf_dom_left 📖	mathematical	Continuous	TopologicalSpace SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	continuous_le_dom inf_le_left
continuous_inf_dom_right 📖	mathematical	Continuous	TopologicalSpace SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	continuous_le_dom inf_le_right
continuous_inf_rng 📖	mathematical	—	Continuous TopologicalSpace SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	—
continuous_le_dom 📖	—	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder Continuous	—	—	continuous_iff_le_induced le_trans
continuous_le_rng 📖	—	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder Continuous	—	—	continuous_iff_coinduced_le le_trans
continuous_nhdsAdjoint_dom 📖	mathematical	—	Continuous nhdsAdjoint Filter.Tendsto nhds	—	gc_nhds nhds_induced
continuous_of_discreteTopology 📖	mathematical	—	Continuous	—	continuous_def isOpen_discrete
continuous_sInf_dom 📖	mathematical	TopologicalSpace Set Set.instMembership Continuous	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	continuous_le_dom sInf_le
continuous_sInf_rng 📖	mathematical	—	Continuous InfSet.sInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	—
continuous_sSup_dom 📖	mathematical	—	Continuous SupSet.sSup TopologicalSpace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	—
continuous_sSup_rng 📖	mathematical	TopologicalSpace Set Set.instMembership Continuous	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	continuous_iff_coinduced_le le_sSup_of_le
continuous_sup_dom 📖	mathematical	—	Continuous TopologicalSpace SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	—
continuous_sup_rng_left 📖	mathematical	Continuous	TopologicalSpace SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	continuous_le_rng le_sup_left
continuous_sup_rng_right 📖	mathematical	Continuous	TopologicalSpace SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	continuous_le_rng le_sup_right
continuous_top 📖	mathematical	—	Continuous Top.top TopologicalSpace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	continuous_iff_coinduced_le le_top
denseRange_discrete 📖	mathematical	—	DenseRange	—	DenseRange.eq_1 dense_discrete Set.range_eq_univ
dense_discrete 📖	mathematical	—	Dense Set.univ	—	IsClosed.closure_eq
discreteTopology_bot 📖	mathematical	—	DiscreteTopology Bot.bot TopologicalSpace OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	—
discreteTopology_iff_forall_isClosed 📖	mathematical	—	DiscreteTopology IsClosed	—	discreteTopology_iff_forall_isOpen Function.Surjective.forall compl_surjective isOpen_compl_iff
discreteTopology_iff_forall_isOpen 📖	mathematical	—	DiscreteTopology IsOpen	—	isOpen_discrete eq_bot_of_singletons_open
discreteTopology_iff_isOpen_singleton 📖	mathematical	—	DiscreteTopology IsOpen Set Set.instSingletonSet	—	isOpen_discrete eq_bot_of_singletons_open
discreteTopology_iff_nhds 📖	mathematical	—	DiscreteTopology nhds Filter Filter.instPure	—	pure_le_nhds
discreteTopology_iff_nhds_ne 📖	mathematical	—	DiscreteTopology nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet Bot.bot Filter Filter.instBot	—	compl_compl
discreteTopology_iff_singleton_mem_nhds 📖	mathematical	—	DiscreteTopology Set Filter Filter.instMembership nhds Set.instSingletonSet	—	—
eq_bot_of_singletons_open 📖	mathematical	IsOpen Set Set.instSingletonSet	Bot.bot TopologicalSpace OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	bot_unique isOpen_biUnion Set.biUnion_of_singleton
forall_open_iff_discrete 📖	mathematical	—	IsOpen DiscreteTopology	—	discreteTopology_iff_forall_isOpen
gc_coinduced_induced 📖	mathematical	—	GaloisConnection TopologicalSpace PartialOrder.toPreorder TopologicalSpace.instPartialOrder TopologicalSpace.coinduced TopologicalSpace.induced	—	coinduced_le_iff_le_induced
gc_nhds 📖	mathematical	—	GaloisConnection Filter TopologicalSpace PartialOrder.toPreorder Filter.instPartialOrder TopologicalSpace.instPartialOrder nhdsAdjoint nhds	—	le_nhds_iff
generateFrom_iInter 📖	mathematical	—	TopologicalSpace.generateFrom Set.iInter Set setOf IsOpen iSup TopologicalSpace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	GaloisCoinsertion.u_iSup_l
generateFrom_iInter_of_generateFrom_eq_self 📖	mathematical	setOf Set IsOpen TopologicalSpace.generateFrom	Set.iInter iSup TopologicalSpace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	GaloisCoinsertion.u_iSup_of_lu_eq_self
generateFrom_iUnion 📖	mathematical	—	TopologicalSpace.generateFrom Set.iUnion Set iInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	GaloisConnection.u_iInf TopologicalSpace.gc_generateFrom
generateFrom_iUnion_isOpen 📖	mathematical	—	TopologicalSpace.generateFrom Set.iUnion Set setOf IsOpen iInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	GaloisCoinsertion.u_iInf_l
generateFrom_insert_empty 📖	mathematical	—	TopologicalSpace.generateFrom Set Set.instInsert Set.instEmptyCollection	—	Set.sUnion_empty generateFrom_insert_of_generateOpen
generateFrom_insert_of_generateOpen 📖	mathematical	TopologicalSpace.GenerateOpen	TopologicalSpace.generateFrom Set Set.instInsert	—	le_antisymm TopologicalSpace.generateFrom_anti Set.subset_insert le_generateFrom TopologicalSpace.isOpen_generateFrom_of_mem
generateFrom_insert_univ 📖	mathematical	—	TopologicalSpace.generateFrom Set Set.instInsert Set.univ	—	generateFrom_insert_of_generateOpen
generateFrom_inter 📖	mathematical	—	TopologicalSpace.generateFrom Set Set.instInter setOf IsOpen TopologicalSpace SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	GaloisCoinsertion.u_sup_l
generateFrom_sUnion 📖	mathematical	—	TopologicalSpace.generateFrom Set.sUnion Set iInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice Set.instMembership	—	GaloisConnection.u_sInf TopologicalSpace.gc_generateFrom
generateFrom_union 📖	mathematical	—	TopologicalSpace.generateFrom Set Set.instUnion TopologicalSpace SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	GaloisConnection.u_inf TopologicalSpace.gc_generateFrom
generateFrom_union_isOpen 📖	mathematical	—	TopologicalSpace.generateFrom Set Set.instUnion setOf IsOpen TopologicalSpace SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	GaloisCoinsertion.u_inf_l
indiscreteTopology_iff 📖	mathematical	—	IndiscreteTopology Top.top TopologicalSpace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—
induced_compose 📖	mathematical	—	TopologicalSpace.induced	—	TopologicalSpace.ext
induced_const 📖	mathematical	—	TopologicalSpace.induced Top.top TopologicalSpace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	le_antisymm le_top Continuous.le_induced continuous_const
induced_generateFrom_eq 📖	mathematical	—	TopologicalSpace.induced TopologicalSpace.generateFrom Set.image Set Set.preimage	—	le_antisymm le_generateFrom Set.forall_mem_image coinduced_le_iff_le_induced Set.mem_image_of_mem
induced_iInf 📖	mathematical	—	TopologicalSpace.induced iInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	GaloisConnection.u_iInf gc_coinduced_induced
induced_id 📖	mathematical	—	TopologicalSpace.induced	—	TopologicalSpace.ext
induced_iff_nhds_eq 📖	mathematical	—	TopologicalSpace.induced nhds Filter.comap	—	nhds_induced
induced_inf 📖	mathematical	—	TopologicalSpace.induced TopologicalSpace SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	GaloisConnection.u_inf gc_coinduced_induced
induced_mono 📖	mathematical	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder	TopologicalSpace.induced	—	GaloisConnection.monotone_u gc_coinduced_induced
induced_sInf 📖	mathematical	—	TopologicalSpace.induced InfSet.sInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice Set.image	—	sInf_eq_iInf' sInf_image' induced_iInf
induced_top 📖	mathematical	—	TopologicalSpace.induced Top.top TopologicalSpace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	GaloisConnection.u_top gc_coinduced_induced
inseparable_top 📖	mathematical	—	Inseparable Top.top TopologicalSpace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	Inseparable.all instIndiscreteTopology
instDiscreteTopologyBool 📖	mathematical	—	DiscreteTopology instTopologicalSpaceBool	—	—
instDiscreteTopologyEmpty 📖	mathematical	—	DiscreteTopology instTopologicalSpaceEmpty	—	—
instDiscreteTopologyFin 📖	mathematical	—	DiscreteTopology instTopologicalSpaceFin	—	—
instDiscreteTopologyInt 📖	mathematical	—	DiscreteTopology instTopologicalSpaceInt	—	—
instDiscreteTopologyNat 📖	mathematical	—	DiscreteTopology instTopologicalSpaceNat	—	—
instDiscreteTopologyPEmpty 📖	mathematical	—	DiscreteTopology instTopologicalSpacePEmpty	—	—
instDiscreteTopologyPUnit 📖	mathematical	—	DiscreteTopology instTopologicalSpacePUnit	—	—
instIndiscreteTopology 📖	mathematical	—	IndiscreteTopology Top.top TopologicalSpace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—
instIndiscreteTopologyEmpty 📖	mathematical	—	IndiscreteTopology instTopologicalSpaceEmpty	—	instIndiscreteTopologyOfSubsingleton
instIndiscreteTopologyOfSubsingleton 📖	mathematical	—	IndiscreteTopology	—	Unique.instSubsingleton
instIndiscreteTopologyPEmpty 📖	mathematical	—	IndiscreteTopology instTopologicalSpacePEmpty	—	instIndiscreteTopologyOfSubsingleton
instIndiscreteTopologyPUnit 📖	mathematical	—	IndiscreteTopology instTopologicalSpacePUnit	—	instIndiscreteTopologyOfSubsingleton
isClosed_coinduced 📖	mathematical	—	IsClosed TopologicalSpace.coinduced Set.preimage	—	isOpen_coinduced
isClosed_discrete 📖	mathematical	—	IsClosed	—	isOpen_discrete
isClosed_iSup_iff 📖	mathematical	—	IsClosed iSup TopologicalSpace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	isOpen_compl_iff
isClosed_induced 📖	mathematical	—	IsClosed TopologicalSpace.induced Set.preimage	—	isOpen_induced IsClosed.isOpen_compl
isClosed_induced_iff 📖	mathematical	—	IsClosed TopologicalSpace.induced Set.preimage	—	Function.Surjective.exists compl_surjective
isClosed_induced_iff' 📖	mathematical	—	IsClosed TopologicalSpace.induced Set Set.instMembership	—	—
isClosed_sSup_iff 📖	mathematical	—	IsClosed SupSet.sSup TopologicalSpace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	sSup_eq_iSup
isOpen_coinduced 📖	mathematical	—	IsOpen TopologicalSpace.coinduced Set.preimage	—	—
isOpen_discrete 📖	mathematical	—	IsOpen	—	DiscreteTopology.eq_bot
isOpen_iSup_iff 📖	mathematical	—	IsOpen iSup TopologicalSpace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	setOf_isOpen_iSup
isOpen_iff_continuous_mem 📖	mathematical	—	IsOpen Continuous sierpinskiSpace Set Set.instMembership	—	continuous_Prop
isOpen_implies_isOpen_iff 📖	mathematical	—	IsOpen TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder	—	—
isOpen_induced 📖	mathematical	IsOpen	TopologicalSpace.induced Set.preimage	—	—
isOpen_induced_eq 📖	mathematical	—	IsOpen TopologicalSpace.induced Set Set.instMembership Set.image Set.preimage setOf	—	—
isOpen_induced_iff 📖	mathematical	—	IsOpen TopologicalSpace.induced Set.preimage	—	—
isOpen_sSup_iff 📖	mathematical	—	IsOpen SupSet.sSup TopologicalSpace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	sSup_eq_iSup
isOpen_singleton_nhdsAdjoint 📖	mathematical	—	IsOpen nhdsAdjoint Set Set.instSingletonSet	—	—
isOpen_singleton_true 📖	mathematical	—	IsOpen sierpinskiSpace Set Set.instSingletonSet	—	Set.mem_singleton
isOpen_sup 📖	mathematical	—	IsOpen TopologicalSpace SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	—
le_generateFrom 📖	mathematical	IsOpen	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder TopologicalSpace.generateFrom	—	TopologicalSpace.le_generateFrom_iff_subset_isOpen
le_iff_nhds 📖	mathematical	—	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder Filter Filter.instPartialOrder nhds	—	nhds_mono le_of_nhds_le_nhds
le_induced_generateFrom 📖	mathematical	IsOpen Set.preimage	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder TopologicalSpace.induced TopologicalSpace.generateFrom	—	induced_generateFrom_eq le_generateFrom
le_nhdsAdjoint_iff 📖	mathematical	—	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder nhdsAdjoint Filter Filter.instPartialOrder nhds Filter.instSup Filter.instPure IsOpen Set Set.instSingletonSet	—	isOpen_singleton_iff_nhds_eq_pure
le_nhdsAdjoint_iff' 📖	mathematical	—	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder nhdsAdjoint Filter Filter.instPartialOrder nhds Filter.instSup Filter.instPure	—	nhds_nhdsAdjoint LE.le.ge_iff_eq' pure_le_nhds
le_of_nhds_le_nhds 📖	mathematical	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhds	TopologicalSpace TopologicalSpace.instPartialOrder	—	isOpen_iff_mem_nhds
map_nhds_induced_eq 📖	mathematical	—	Filter.map nhds TopologicalSpace.induced nhdsWithin Set.range	—	nhds_induced Filter.map_comap nhdsWithin.eq_1
map_nhds_induced_of_mem 📖	mathematical	Set Filter Filter.instMembership nhds Set.range	Filter.map TopologicalSpace.induced	—	nhds_induced Filter.map_comap_of_mem
map_nhds_induced_of_surjective 📖	mathematical	—	Filter.map nhds TopologicalSpace.induced	—	nhds_induced Filter.map_comap_of_surjective
mem_nhds_discrete 📖	mathematical	—	Set Filter Filter.instMembership nhds Set.instMembership	—	nhds_discrete Filter.mem_pure
mem_nhds_induced 📖	mathematical	—	Set Filter Filter.instMembership nhds TopologicalSpace.induced Set.instHasSubset Set.preimage	—	Set.Subset.rfl HasSubset.Subset.trans Set.instIsTransSubset Set.preimage_mono
nhds_discrete 📖	mathematical	—	nhds Filter Filter.instPure	—	le_antisymm IsOpen.mem_nhds isOpen_discrete pure_le_nhds
nhds_false 📖	mathematical	—	nhds sierpinskiSpace Top.top Filter Filter.instTop	—	TopologicalSpace.nhds_generateFrom iInf_congr_Prop Filter.principal_singleton instIsEmptyFalse
nhds_iInf 📖	mathematical	—	nhds iInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice Filter Filter.instInfSet	—	GaloisConnection.u_iInf gc_nhds
nhds_induced 📖	mathematical	—	nhds TopologicalSpace.induced Filter.comap	—	Filter.ext mem_nhds_induced Filter.mem_comap
nhds_inf 📖	mathematical	—	nhds TopologicalSpace SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice Filter Filter.instInf	—	GaloisConnection.u_inf gc_nhds
nhds_mono 📖	mathematical	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder	Filter Filter.instPartialOrder nhds	—	GaloisConnection.monotone_u gc_nhds
nhds_nhdsAdjoint 📖	mathematical	—	nhds nhdsAdjoint Function.update Filter Filter.instPure Filter.instSup	—	Function.eq_update_iff nhds_nhdsAdjoint_same nhds_nhdsAdjoint_of_ne
nhds_nhdsAdjoint_of_ne 📖	mathematical	—	nhds nhdsAdjoint Filter Filter.instPure	—	isOpen_singleton_iff_nhds_eq_pure isOpen_singleton_nhdsAdjoint
nhds_nhdsAdjoint_same 📖	mathematical	—	nhds nhdsAdjoint Filter Filter.instSup Filter.instPure	—	le_antisymm IsOpen.mem_nhds sup_le pure_le_nhds GaloisConnection.le_u_l gc_nhds
nhds_sInf 📖	mathematical	—	nhds InfSet.sInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice iInf Filter Filter.instInfSet Set Set.instMembership	—	GaloisConnection.u_sInf gc_nhds
nhds_top 📖	mathematical	—	nhds Top.top TopologicalSpace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Filter Filter.instTop	—	GaloisConnection.u_top gc_nhds
nhds_true 📖	mathematical	—	nhds sierpinskiSpace Filter Filter.instPure	—	le_antisymm Filter.le_pure_iff IsOpen.mem_nhds isOpen_singleton_true Set.mem_singleton pure_le_nhds
nontrivialTopology_iff 📖	mathematical	—	NontrivialTopology	—	—
preimage_nhds_coinduced 📖	mathematical	Set Filter Filter.instMembership nhds TopologicalSpace.coinduced	Set.preimage	—	mem_nhds_iff Set.preimage_mono
setOf_isOpen_iSup 📖	mathematical	—	setOf Set IsOpen iSup TopologicalSpace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice Set.iInter	—	GaloisConnection.l_iSup TopologicalSpace.gc_generateFrom
setOf_isOpen_sSup 📖	mathematical	—	setOf Set IsOpen SupSet.sSup TopologicalSpace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice Set.iInter Set.instMembership	—	GaloisConnection.l_sSup TopologicalSpace.gc_generateFrom
setOf_isOpen_sup 📖	mathematical	—	setOf Set IsOpen TopologicalSpace SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice Set.instInter	—	—
singletons_open_iff_discrete 📖	mathematical	—	IsOpen Set Set.instSingletonSet DiscreteTopology	—	discreteTopology_iff_isOpen_singleton
tendsto_nhds_Prop 📖	mathematical	—	Filter.Tendsto nhds sierpinskiSpace Filter.Eventually	—	nhds_true nhds_false instIsEmptyFalse
tendsto_nhds_true 📖	mathematical	—	Filter.Tendsto nhds sierpinskiSpace Filter.Eventually	—	nhds_true

closure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mono 📖	mathematical	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder	Set Set.instHasSubset closure	—	closure_minimal subset_closure IsClosed.mono isClosed_closure

---

← Back to Index