Hausdorff

📁 Source: Mathlib/Topology/Separation/Hausdorff.lean

Statistics

Metric	Count
Definitions `T2Quotient`, `instTopologicalSpace`, `mk`, `T2Space`, `t2Setoid`	5
Theorems `isClosed`, `ext_on`, `isClosedEmbedding`, `isClosedMap`, `limUnder_eq`, `eventuallyEq_nhds_iff_eventuallyEq_nhdsNE`, `ne_iff_eventually_ne`, `toT2Space`, `limUnder_eq`, `limUnder_eq_iff`, `isClosedEmbedding`, `isClosed_range`, `t2Space`, `isClosed_eq`, `disjoint_nhdsSet_nhds`, `inter`, `isClosed`, `nhdsSet_inter_eq`, `preimage_continuous`, `separation_of_notMem`, `subsingleton`, `of_surjective_continuous`, `isCompact_closure_iff`, `isCompact_iff`, `t2Space`, `t2Space`, `t2Space_iff_t0Space`, `of_finset_finset`, `of_isClosed_isCompact_closure_compl_isClosed`, `of_isCompact_isCompact`, `of_singleton_finset`, `t2Space`, `t2Space_iff`, `closure`, `of_subset_closure`, `t2_separation`, `exists_isOpen_superset`, `exists_mem_nhdsSet`, `pairwiseDisjoint_nhds`, `t2Space`, `compatible`, `continuous_lift`, `continuous_mk`, `inductionOn`, `inductionOn₂`, `instT2Space`, `lift_mk`, `mk_eq`, `surjective_mk`, `unique_lift`, `of_injective_continuous`, `r1Space`, `t1Space`, `t2`, `t2Space`, `instT2Space`, `lim_eq_iff_le_nhds`, `disjoint_nhds_nhds`, `eqOn_closure₂`, `eqOn_closure₂'`, `eq_of_nhds_neBot`, `exists_subset_nhds_of_isCompact`, `image_closure_of_isCompact`, `instT2SpaceOfR1SpaceOfT0Space`, `instT2SpaceSubtype`, `instT2SpaceSum`, `isClosed_diagonal`, `isClosed_eq`, `isIrreducible_iff_singleton`, `isOpen_iff_ultrafilter'`, `isOpen_ne_fun`, `isPreirreducible_iff_forall_mem_subset_closure_singleton`, `isPreirreducible_iff_subsingleton`, `limUnder_nhdsWithin_id`, `limUnder_nhds_id`, `lim_eq`, `lim_eq_iff`, `lim_nhds`, `lim_nhdsWithin`, `not_preirreducible_nontrivial_t2`, `pairwise_disjoint_nhds`, `separated_by_continuous`, `separated_by_isOpenEmbedding`, `t2Space_antitone`, `t2Space_iff`, `t2Space_iff_disjoint_nhds`, `t2Space_iff_nhds`, `t2Space_iff_of_isOpenQuotientMap`, `t2_iff_isClosed_diagonal`, `t2_iff_nhds`, `t2_iff_ultrafilter`, `t2_separation`, `t2_separation_compact_nhds`, `t2_separation_nhds`, `tendsto_nhds_unique`, `tendsto_nhds_unique'`, `tendsto_nhds_unique_of_eventuallyEq`, `tendsto_nhds_unique_of_frequently_eq`	98
Total	103

CompactExhaustion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isClosed` 📖	mathematical	—	`IsClosed` `DFunLike.coe` `CompactExhaustion` `Set` `instFunLikeNatSet`	—	`IsCompact.isClosed` `isCompact`

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext_on` 📖	—	`Dense` `Continuous` `Set.EqOn`	—	—	`Set.EqOn.closure`
`isClosedEmbedding` 📖	mathematical	`Continuous`	`Topology.IsClosedEmbedding`	—	`Topology.IsClosedEmbedding.of_continuous_injective_isClosedMap` `isClosedMap`
`isClosedMap` 📖	mathematical	`Continuous`	`IsClosedMap`	—	`IsCompact.isClosed` `IsCompact.image` `IsClosed.isCompact`
`limUnder_eq` 📖	mathematical	`Continuous`	`limUnder` `nhds`	—	`Filter.Tendsto.limUnder_eq` `nhds_neBot` `tendsto`

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventuallyEq_nhds_iff_eventuallyEq_nhdsNE` 📖	mathematical	`ContinuousAt`	`Filter.EventuallyEq` `nhdsWithin` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `nhds`	—	`eventuallyEq_nhds_of_eventuallyEq_nhdsNE` `Filter.Eventually.and` `eventually_nhdsWithin_of_eventually_nhds` `ne_iff_eventually_ne` `Filter.empty_notMem` `Filter.EventuallyEq.filter_mono` `nhdsWithin_le_nhds`
`ne_iff_eventually_ne` 📖	mathematical	`ContinuousAt`	`Filter.Eventually` `nhds`	—	`t2_separation` `Filter.mp_mem` `Filter.inter_mem` `preimage_mem_nhds` `IsOpen.mem_nhds` `Filter.univ_mem'` `Set.disjoint_iff_inter_eq_empty` `eventually_nhds_iff`

DiscreteTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toT2Space` 📖	mathematical	—	`T2Space`	—	`isOpen_discrete` `Set.disjoint_singleton`

Filter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`limUnder_eq_iff` 📖	mathematical	`Tendsto` `nhds`	`limUnder`	—	`tendsto_nhds_limUnder` `Tendsto.limUnder_eq`

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`limUnder_eq` 📖	mathematical	`Filter.Tendsto` `nhds`	`limUnder`	—	`lim_eq` `Filter.map_neBot`

Function.LeftInverse

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isClosedEmbedding` 📖	mathematical	`Continuous`	`Topology.IsClosedEmbedding`	—	`Topology.IsEmbedding.of_leftInverse` `isClosed_range`
`isClosed_range` 📖	mathematical	`Continuous`	`IsClosed` `Set.range`	—	`Set.EqOn.closure` `Set.RightInvOn.eqOn` `rightInvOn_range` `Continuous.comp` `continuous_id` `isClosed_of_closure_subset`

Homeomorph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`t2Space` 📖	mathematical	—	`T2Space`	—	`Topology.IsEmbedding.t2Space` `isEmbedding`

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isClosed_eq` 📖	mathematical	`ContinuousOn`	`IsClosed` `setOf` `Set` `Set.instMembership`	—	`ContinuousOn.preimage_isClosed_of_isClosed` `ContinuousOn.prodMk` `isClosed_diagonal`

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjoint_nhdsSet_nhds` 📖	mathematical	`IsCompact` `Set` `Set.instMembership`	`Disjoint` `Filter` `Filter.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Filter.instCompleteLatticeFilter` `nhdsSet` `nhds`	—	`nhdsSet_singleton` `SeparatedNhds.disjoint_nhdsSet` `SeparatedNhds.of_isCompact_isCompact_isClosed` `T2Space.r1Space` `isCompact_singleton` `isClosed_singleton` `T2Space.t1Space` `Set.disjoint_singleton_right`
`inter` 📖	mathematical	`IsCompact`	`Set` `Set.instInter`	—	`inter_right` `isClosed`
`isClosed` 📖	mathematical	`IsCompact`	`IsClosed`	—	`isClosed_iff_forall_filter` `exists_clusterPt` `Set.mem_of_eq_of_mem` `eq_of_nhds_neBot` `ClusterPt.neBot` `ClusterPt.mono`
`nhdsSet_inter_eq` 📖	mathematical	`IsCompact`	`nhdsSet` `Set` `Set.instInter` `Filter` `Filter.instInf`	—	`le_antisymm` `nhdsSet_inter_le` `nhdsSet_inf_eq_biSup` `iSup_congr_Prop` `inf_nhdsSet_eq_biSup` `sSup_image` `iSup₂_le` `eq_or_ne` `le_iSup₂_of_le` `Eq.le` `inf_idem` `bot_le` `Disjoint.eq_bot` `disjoint_nhds_nhds`
`preimage_continuous` 📖	mathematical	`IsCompact` `Continuous`	`Set.preimage`	—	`IsClosed.isCompact` `IsClosed.preimage` `isClosed`
`separation_of_notMem` 📖	mathematical	`IsCompact` `Set` `Set.instMembership`	`IsOpen` `Set.instHasSubset` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`SeparatedNhds.of_isCompact_isCompact_isClosed` `T2Space.r1Space` `isCompact_singleton` `isClosed_singleton` `T2Space.t1Space` `Set.disjoint_singleton_right`

IsPreirreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`subsingleton` 📖	mathematical	`IsPreirreducible`	`Set.Subsingleton`	—	`isPreirreducible_iff_subsingleton`

IsQuotientMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_surjective_continuous` 📖	mathematical	`Continuous`	`Topology.IsQuotientMap`	—	`IsClosedMap.isQuotientMap` `Continuous.isClosedMap`

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCompact_closure_iff` 📖	mathematical	`R1Space`	`IsCompact` `topologicalSpace` `closure` `Set.image` `Function.eval`	—	`instR1SpaceForall`
`isCompact_iff` 📖	mathematical	`T2Space`	`IsCompact` `topologicalSpace` `IsClosed` `Set.image` `Function.eval`	—	`IsCompact.isClosed` `t2Space` `IsCompact.image` `continuous_apply` `IsCompact.of_isClosed_subset` `isCompact_univ_pi` `Set.subset_pi_eval_image`
`t2Space` 📖	mathematical	`T2Space`	`topologicalSpace`	—	`instT2SpaceOfR1SpaceOfT0Space` `instR1SpaceForall` `T2Space.r1Space` `instT0Space` `T1Space.t0Space` `T2Space.t1Space`

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`t2Space` 📖	mathematical	—	`T2Space` `instTopologicalSpaceProd`	—	`instT2SpaceOfR1SpaceOfT0Space` `instR1SpaceProd` `T2Space.r1Space` `instT0Space` `T1Space.t0Space` `T2Space.t1Space`

R1Space

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`t2Space_iff_t0Space` 📖	mathematical	—	`T2Space` `T0Space`	—	`T1Space.t0Space` `T2Space.t1Space` `instT2SpaceOfR1SpaceOfT0Space`

SeparatedNhds

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_finset_finset` 📖	mathematical	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot`	`SeparatedNhds` `SetLike.coe` `Finset.instSetLike`	—	`of_isCompact_isCompact` `Set.Finite.isCompact` `Finset.finite_toSet`
`of_isClosed_isCompact_closure_compl_isClosed` 📖	mathematical	`IsCompact` `closure` `Compl.compl` `Set` `Set.instCompl` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`SeparatedNhds`	—	`IsCompact.of_isClosed_subset` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Disjoint.subset_compl_left` `subset_closure` `Set.diff_union_of_subset` `interior_subset` `union_left` `IsClosed.frontier_eq` `frontier_eq_closure_inter_closure` `IsClosed.closure_eq` `of_isCompact_isCompact_isClosed` `IsClosed.inter` `isClosed_closure` `Set.inter_subset_right` `Set.disjoint_of_subset_left` `Set.inter_subset_left` `isOpen_interior` `IsClosed.isOpen_compl` `le_rfl` `Disjoint.mono_left` `disjoint_compl_right`
`of_isCompact_isCompact` 📖	mathematical	`IsCompact` `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`	`SeparatedNhds`	—	`Set.prod_subset_compl_diagonal_iff_disjoint` `generalized_tube_lemma` `IsClosed.isOpen_compl` `isClosed_diagonal`
`of_singleton_finset` 📖	mathematical	`Finset` `Finset.instMembership`	`SeparatedNhds` `Set` `Set.instSingletonSet` `SetLike.coe` `Finset.instSetLike`	—	`Finset.coe_singleton` `of_finset_finset` `Finset.disjoint_singleton_left`

SeparationQuotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`t2Space` 📖	mathematical	—	`T2Space` `SeparationQuotient` `instTopologicalSpaceSeparationQuotient`	—	`t2Space_iff`
`t2Space_iff` 📖	mathematical	—	`T2Space` `SeparationQuotient` `instTopologicalSpaceSeparationQuotient` `R1Space`	—	`Filter.disjoint_comap_iff` `Function.Surjective.forall₂`

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pairwiseDisjoint_nhds` 📖	mathematical	—	`PairwiseDisjoint` `Filter` `Filter.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Filter.instCompleteLatticeFilter` `nhds`	—	`Pairwise.set_pairwise` `pairwise_disjoint_nhds`

Set.EqOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure` 📖	mathematical	`Set.EqOn` `Continuous`	`closure`	—	`closure_minimal` `isClosed_eq`
`of_subset_closure` 📖	—	`Set.EqOn` `ContinuousOn` `Set` `Set.instHasSubset` `closure`	—	—	`mem_closure_iff_clusterPt` `tendsto_nhds_unique_of_eventuallyEq` `Filter.Tendsto.mono_left` `nhdsWithin_mono` `eventuallyEq_of_mem` `self_mem_nhdsWithin`

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`t2_separation` 📖	mathematical	—	`Set` `Set.instMembership` `IsOpen` `Set.PairwiseDisjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`Set.PairwiseDisjoint.exists_mem_filter_basis` `Set.pairwiseDisjoint_nhds` `nhds_basis_opens`

Set.InjOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isOpen_superset` 📖	mathematical	`Set.InjOn` `IsCompact` `ContinuousAt` `Set` `Filter` `Filter.instMembership` `nhds`	`IsOpen` `Set.instHasSubset`	—	`exists_mem_nhdsSet` `mem_nhdsSet_iff_exists` `mono`
`exists_mem_nhdsSet` 📖	mathematical	`Set.InjOn` `IsCompact` `ContinuousAt` `Set` `Filter` `Filter.instMembership` `nhds`	`nhdsSet`	—	`eq_or_ne` `Filter.mem_of_superset` `prod_mem_nhds` `Set.forall_prod_set` `ContinuousAt.prodMap'` `IsOpen.mem_nhds` `IsClosed.isOpen_compl` `isClosed_diagonal` `ne` `Filter.Eventually.mono` `Filter.eventually_prod_self_iff` `IsCompact.nhdsSet_prod_eq` `eventually_nhdsSet_iff_forall`

Sigma

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`t2Space` 📖	mathematical	`T2Space`	`instTopologicalSpaceSigma`	—	`eq_or_ne` `separated_by_isOpenEmbedding` `Topology.IsOpenEmbedding.sigmaMk` `separated_by_continuous` `DiscreteTopology.toT2Space` `continuous_def` `isOpen_sigma_fst_preimage`

T2Quotient

Definitions

Name	Category	Theorems
`instTopologicalSpace` 📖	CompOp	3 math math: `instT2Space`, `continuous_lift`, `continuous_mk`
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compatible` 📖	—	`Continuous` `t2Setoid`	—	—	`sInf_le` `T2Space.of_injective_continuous` `Setoid.kerLift_injective` `Continuous.quotient_lift`
`continuous_lift` 📖	mathematical	`Continuous`	`T2Quotient` `instTopologicalSpace` `lift`	—	`continuous_coinduced_dom`
`continuous_mk` 📖	mathematical	—	`Continuous` `T2Quotient` `instTopologicalSpace`	—	`continuous_quotient_mk'`
`inductionOn` 📖	—	—	—	—	—
`inductionOn₂` 📖	—	—	—	—	—
`instT2Space` 📖	mathematical	—	`T2Space` `T2Quotient` `instTopologicalSpace`	—	`t2Space_iff` `separated_by_continuous` `continuous_map_sInf`
`lift_mk` 📖	mathematical	`Continuous`	`lift`	—	`compatible`
`mk_eq` 📖	—	—	—	—	`Setoid.quotient_mk_sInf_eq`
`surjective_mk` 📖	mathematical	—	`T2Quotient`	—	`Quotient.mk_surjective`
`unique_lift` 📖	mathematical	`Continuous` `T2Quotient`	`lift`	—	`Function.Surjective.right_cancellable` `lift.congr_simp`

T2Space

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_injective_continuous` 📖	mathematical	`Continuous`	`T2Space`	—	`separated_by_continuous`
`r1Space` 📖	mathematical	—	`R1Space`	—	`specializes_of_eq` `disjoint_nhds_nhds` `eq_or_ne`
`t1Space` 📖	mathematical	—	`T1Space`	—	`t1Space_iff_disjoint_pure_nhds` `Disjoint.mono_left` `pure_le_nhds` `disjoint_nhds_nhds`
`t2` 📖	mathematical	—	`Pairwise` `Set` `IsOpen` `Set.instMembership` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	—

Topology.IsEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`t2Space` 📖	mathematical	`Topology.IsEmbedding`	`T2Space`	—	`T2Space.of_injective_continuous` `injective` `continuous`

ULift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instT2Space` 📖	mathematical	—	`T2Space` `topologicalSpace`	—	`Topology.IsEmbedding.t2Space` `Topology.IsEmbedding.uliftDown`

Ultrafilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lim_eq_iff_le_nhds` 📖	mathematical	—	`lim` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `toFilter` `nhds`	—	`le_nhds_lim` `lim_eq` `neBot`

(root)

Definitions

Name	Category	Theorems
`T2Quotient` 📖	CompOp	4 math math: `T2Quotient.instT2Space`, `T2Quotient.continuous_lift`, `T2Quotient.continuous_mk`, `T2Quotient.surjective_mk`
`T2Space` 📖	CompData	85 math math: `SeparationQuotient.t2Space`, `ContinuousLinearMap.instT2Space`, `CategoryTheory.PreGaloisCategory.instT2SpaceAutFunctorFintypeCat`, `AddGroupFilterBasis.t2Space_iff`, `MeasureTheory.FiniteMeasure.t2Space`, `AddOpposite.instT2Space`, `EReal.instT2Space`, `Compactum.instT2SpaceA`, `t2Space_antitone`, `instT2SpaceStoneCech`, `IsTopologicalGroup.t2Space_of_one_sep`, `T2Quotient.instT2Space`, `instT2SpaceOfR1SpaceOfT0Space`, `IsAdic.isAdicComplete_iff`, `GroupFilterBasis.t2Space_iff_sInter_subset`, `PowerSeries.WithPiTopology.instT2Space`, `DiscreteTopology.toT2Space`, `t2Space_of_properVAdd_of_t1AddGroup`, `T2Space.of_injective_continuous`, `R1Space.t2Space_iff_t0Space`, `TrivSqZeroExt.instT2Space`, `UniformFun.instT2Space`, `PointwiseConvergenceCLM.instT2Space`, `Metric.Snowflaking.instT2Space`, `OrderClosedTopology.to_t2Space`, `QuotientGroup.instT2Space`, `QuotientAddGroup.instT2Space`, `CommRingCat.HomTopology.instT2SpaceHomOfCarrier`, `t2space_iff_isSeparatedMap`, `t2Space_quotient_addAction_of_properVAdd`, `CompHausLike.instT2SpaceCarrierObjTopCatCompHausLikeToTop`, `UniformConvergenceCLM.t2Space`, `DomMulAct.instT2Space`, `MvPowerSeries.WithPiTopology.instT2Space`, `UniformOnFun.t2Space_of_covering`, `t2Space_of_properlyDiscontinuousVAdd_of_t2Space`, `t2_iff_isClosed_diagonal`, `MeasureTheory.ProbabilityMeasure.t2Space`, `t2Space_iff_disjoint_nhds`, `WeakDual.instT2Space`, `CStarMatrix.instT2Space`, `IsTopologicalGroup.t2Space_iff_one_closed`, `AddUnits.instT2Space`, `Prod.t2Space`, `Units.instT2Space`, `ContinuousMap.instT2Space`, `T25Space.t2Space`, `ULift.instT2Space`, `t2Space_iff_nhds`, `ContinuousMapZero.instT2Space`, `Complex.instT2Space`, `ContinuousMonoidHom.instT2Space`, `t2Space_quotient_mulAction_of_properSMul`, `ContinuousMultilinearMap.instT2Space`, `Ultrafilter.t2Space`, `TotallySeparatedSpace.t2Space`, `CompactConvergenceCLM.instT2Space`, `instT2SpaceSubtype`, `ConnectedComponents.t2`, `ContinuousAddMonoidHom.instT2Space`, `SeparatingDual.t2Space`, `t2Space_iff_of_isOpenQuotientMap`, `IsTopologicalAddGroup.t2Space_of_zero_sep`, `instT2SpaceSum`, `IsTopologicalAddGroup.t2Space_iff_zero_closed`, `TopologicalSpace.t2Space_of_metrizableSpace`, `ContinuousAlternatingMap.instT2Space`, `instT2SpaceMatrix`, `SeparationQuotient.t2Space_iff`, `t2_iff_ultrafilter`, `krullTopology_t2`, `IsAdic.isHausdorff_iff`, `t2_iff_nhds`, `CompHausLike.is_hausdorff`, `Topology.IsEmbedding.t2Space`, `AddGroupFilterBasis.t2Space_iff_sInter_subset`, `Homeomorph.t2Space`, `ENNReal.instT2Space`, `GroupFilterBasis.t2Space_iff`, `MulOpposite.instT2Space`, `t2Space_iff`, `t2Space_of_properlyDiscontinuousSMul_of_t2Space`, `t2Space_of_properSMul_of_t1Group`, `DomAddAct.instT2Space`, `CompHaus.instT2SpaceCarrierToTopTrue`
`t2Setoid` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjoint_nhds_nhds` 📖	mathematical	—	`Disjoint` `Filter` `Filter.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Filter.instCompleteLatticeFilter` `nhds`	—	`Filter.NeBot.ne` `nhds_neBot` `t2Space_iff_disjoint_nhds`
`eqOn_closure₂` 📖	—	`Continuous` `instTopologicalSpaceProd` `Set` `Set.instMembership` `closure`	—	—	`eqOn_closure₂'` `Continuous.uncurry_left` `Continuous.uncurry_right`
`eqOn_closure₂'` 📖	—	`Continuous` `Set` `Set.instMembership` `closure`	—	—	`closure_minimal` `Set.mem_iInter₂` `Set.EqOn.closure` `isClosed_biInter` `isClosed_eq`
`eq_of_nhds_neBot` 📖	—	—	—	—	`t2_iff_nhds`
`exists_subset_nhds_of_isCompact` 📖	—	`Directed` `Set` `Set.instHasSubset` `IsCompact` `Filter` `Filter.instMembership` `nhds`	—	—	`exists_subset_nhds_of_isCompact'` `IsCompact.isClosed`
`image_closure_of_isCompact` 📖	mathematical	`IsCompact` `closure` `ContinuousOn`	`Set.image`	—	`Set.Subset.antisymm` `ContinuousOn.image_closure` `closure_minimal` `Set.image_mono` `subset_closure` `IsCompact.isClosed` `IsCompact.image_of_continuousOn`
`instT2SpaceOfR1SpaceOfT0Space` 📖	mathematical	—	`T2Space`	—	`t2Space_iff_disjoint_nhds` `disjoint_nhds_nhds_iff_not_inseparable` `Inseparable.eq`
`instT2SpaceSubtype` 📖	mathematical	—	`T2Space` `instTopologicalSpaceSubtype`	—	`instT2SpaceOfR1SpaceOfT0Space` `instR1SpaceSubtype` `T2Space.r1Space` `Subtype.t0Space` `T1Space.t0Space` `T2Space.t1Space`
`instT2SpaceSum` 📖	mathematical	—	`T2Space` `instTopologicalSpaceSum`	—	`separated_by_isOpenEmbedding` `Topology.IsOpenEmbedding.inl` `separated_by_continuous` `DiscreteTopology.toT2Space` `instDiscreteTopologyBool` `continuous_isLeft` `Topology.IsOpenEmbedding.inr`
`isClosed_diagonal` 📖	mathematical	—	`IsClosed` `instTopologicalSpaceProd` `Set.diagonal`	—	`t2_iff_isClosed_diagonal`
`isClosed_eq` 📖	mathematical	`Continuous`	`IsClosed` `setOf`	—	`continuous_iff_isClosed` `Continuous.prodMk` `isClosed_diagonal`
`isIrreducible_iff_singleton` 📖	mathematical	—	`IsIrreducible` `Set` `Set.instSingletonSet`	—	`IsIrreducible.eq_1` `isPreirreducible_iff_subsingleton` `Set.exists_eq_singleton_iff_nonempty_subsingleton`
`isOpen_iff_ultrafilter'` 📖	mathematical	—	`IsOpen` `Set` `Filter` `Filter.instMembership` `Ultrafilter.toFilter`	—	`isOpen_iff_ultrafilter` `Ultrafilter.le_nhds_lim` `Ultrafilter.lim_eq_iff_le_nhds`
`isOpen_ne_fun` 📖	mathematical	`Continuous`	`IsOpen` `setOf`	—	`isOpen_compl_iff` `isClosed_eq`
`isPreirreducible_iff_forall_mem_subset_closure_singleton` 📖	mathematical	—	`IsPreirreducible` `Set` `Set.instHasSubset` `closure` `Set.instSingletonSet`	—	`r1_separation` `Specializes.mem_closure` `Inseparable.specializes` `Set.Nonempty.not_disjoint` `Set.Nonempty.mono` `Set.inter_subset_right` `Specializes.mem_open` `specializes_iff_mem_closure`
`isPreirreducible_iff_subsingleton` 📖	mathematical	—	`IsPreirreducible` `Set.Subsingleton`	—	`T2Space.r1Space` `IsClosed.closure_eq` `T2Space.t1Space`
`limUnder_nhdsWithin_id` 📖	mathematical	`Set` `Set.instMembership` `closure`	`limUnder` `nhdsWithin`	—	`lim_nhdsWithin`
`limUnder_nhds_id` 📖	mathematical	—	`limUnder` `nhds`	—	`lim_nhds`
`lim_eq` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhds`	`lim`	—	`tendsto_nhds_unique` `le_nhds_lim`
`lim_eq_iff` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhds`	`lim`	—	`le_nhds_lim` `lim_eq`
`lim_nhds` 📖	mathematical	—	`lim` `nhds`	—	`lim_eq` `nhds_neBot` `le_rfl`
`lim_nhdsWithin` 📖	mathematical	`Set` `Set.instMembership` `closure`	`lim` `nhdsWithin`	—	`lim_eq` `mem_closure_iff_clusterPt` `inf_le_left`
`not_preirreducible_nontrivial_t2` 📖	—	—	—	—	`Set.Subsingleton.not_nontrivial` `IsPreirreducible.subsingleton` `PreirreducibleSpace.isPreirreducible_univ` `Set.nontrivial_univ`
`pairwise_disjoint_nhds` 📖	mathematical	—	`Pairwise` `Function.onFun` `Filter` `Disjoint` `Filter.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Filter.instCompleteLatticeFilter` `nhds`	—	`disjoint_nhds_nhds`
`separated_by_continuous` 📖	mathematical	`Continuous`	`IsOpen` `Set` `Set.instMembership` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`t2_separation` `IsOpen.preimage` `Disjoint.preimage`
`separated_by_isOpenEmbedding` 📖	mathematical	`Topology.IsOpenEmbedding`	`IsOpen` `Set` `Set.instMembership` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`t2_separation` `Topology.IsOpenEmbedding.isOpenMap` `Set.mem_image_of_mem` `Set.disjoint_image_of_injective` `Topology.IsEmbedding.injective` `Topology.IsOpenEmbedding.toIsEmbedding`
`t2Space_antitone` 📖	mathematical	—	`Antitone` `TopologicalSpace` `PartialOrder.toPreorder` `TopologicalSpace.instPartialOrder` `Prop.partialOrder` `T2Space`	—	`T2Space.of_injective_continuous` `continuous_id_of_le`
`t2Space_iff` 📖	mathematical	—	`T2Space` `Pairwise` `Set` `IsOpen` `Set.instMembership` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	—
`t2Space_iff_disjoint_nhds` 📖	mathematical	—	`T2Space` `Pairwise` `Disjoint` `Filter` `Filter.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Filter.instCompleteLatticeFilter` `nhds`	—	`t2Space_iff` `Filter.HasBasis.disjoint_iff` `nhds_basis_opens`
`t2Space_iff_nhds` 📖	mathematical	—	`T2Space` `Pairwise` `Set` `Filter` `Filter.instMembership` `nhds` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	—
`t2Space_iff_of_isOpenQuotientMap` 📖	mathematical	`IsOpenQuotientMap`	`T2Space` `IsClosed` `instTopologicalSpaceProd` `setOf`	—	`t2_iff_isClosed_diagonal` `IsOpenQuotientMap.prodMap` `IsClosed.preimage` `IsOpenQuotientMap.continuous` `Function.Surjective.image_preimage` `IsOpenQuotientMap.surjective` `IsOpenQuotientMap.isOpenMap`
`t2_iff_isClosed_diagonal` 📖	mathematical	—	`T2Space` `IsClosed` `instTopologicalSpaceProd` `Set.diagonal`	—	`nhds_prod_eq`
`t2_iff_nhds` 📖	mathematical	—	`T2Space`	—	—
`t2_iff_ultrafilter` 📖	mathematical	—	`T2Space`	—	`t2_iff_nhds`
`t2_separation` 📖	mathematical	—	`IsOpen` `Set` `Set.instMembership` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`T2Space.t2`
`t2_separation_compact_nhds` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `IsCompact` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`Filter.HasBasis.disjoint_iff` `compact_basis_nhds` `disjoint_nhds_nhds`
`t2_separation_nhds` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`t2_separation` `IsOpen.mem_nhds`
`tendsto_nhds_unique` 📖	—	`Filter.Tendsto` `nhds`	—	—	`Inseparable.eq` `T1Space.t0Space` `T2Space.t1Space` `tendsto_nhds_unique_inseparable` `T2Space.r1Space`
`tendsto_nhds_unique'` 📖	—	`Filter.Tendsto` `nhds`	—	—	`tendsto_nhds_unique`
`tendsto_nhds_unique_of_eventuallyEq` 📖	—	`Filter.Tendsto` `nhds` `Filter.EventuallyEq`	—	—	`tendsto_nhds_unique` `Filter.Tendsto.congr'`
`tendsto_nhds_unique_of_frequently_eq` 📖	—	`Filter.Tendsto` `nhds` `Filter.Frequently`	—	—	`Filter.Tendsto.frequently` `Filter.Tendsto.prodMk_nhds` `IsOpen.mem_nhds` `IsClosed.isOpen_compl` `isClosed_diagonal`

---

← Back to Index