UrysohnsLemma

📁 Source: Mathlib/Topology/UrysohnsLemma.lean

Statistics

Metric	Count
Definitions CU, C, U, approx, left, lim, right	7
Theorems P_C_U, approx_le_approx_of_U_sub_C, approx_le_lim, approx_le_one, approx_le_succ, approx_mem_Icc_right_left, approx_mono, approx_nonneg, approx_of_mem_C, approx_of_notMem_U, bddAbove_range_approx, closed_C, continuous_lim, disjoint_C_support_lim, hP, left_C, left_U_subset, left_U_subset_right_C, lim_eq_midpoint, lim_le_one, lim_mem_Icc, lim_nonneg, lim_of_mem_C, lim_of_notMem_U, open_U, right_U, subset, subset_right_C, tendsto_approx_atTop, exists_continuousMap_one_of_isCompact_subset_isOpen, exists_continuous_nonneg_pos, exists_continuous_one_zero_of_isCompact, exists_continuous_one_zero_of_isCompact_of_isGδ, exists_continuous_zero_one_of_isClosed, exists_continuous_zero_one_of_isCompact, exists_continuous_zero_one_of_isCompact', exists_tsupport_one_of_isOpen_isClosed	37
Total	44

Urysohns

Definitions

Name	Category	Theorems
CU 📖	CompData	—

Urysohns.CU

Definitions

Name	Category	Theorems
C 📖	CompOp	7 math math: subset_right_C, closed_C, left_U_subset_right_C, P_C_U, left_C, disjoint_C_support_lim, subset
U 📖	CompOp	6 math math: left_U_subset_right_C, right_U, P_C_U, open_U, subset, left_U_subset
approx 📖	CompOp	11 math math: approx_of_mem_C, approx_le_succ, approx_nonneg, approx_mono, bddAbove_range_approx, approx_mem_Icc_right_left, approx_le_one, approx_le_approx_of_U_sub_C, approx_of_notMem_U, approx_le_lim, tendsto_approx_atTop
left 📖	CompOp	5 math math: left_U_subset_right_C, approx_mem_Icc_right_left, left_C, left_U_subset, lim_eq_midpoint
lim 📖	CompOp	10 math math: lim_le_one, lim_of_mem_C, continuous_lim, lim_of_notMem_U, disjoint_C_support_lim, lim_nonneg, lim_mem_Icc, lim_eq_midpoint, approx_le_lim, tendsto_approx_atTop
right 📖	CompOp	5 math math: subset_right_C, left_U_subset_right_C, approx_mem_Icc_right_left, right_U, lim_eq_midpoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
P_C_U 📖	mathematical	—	C U	—	—
approx_le_approx_of_U_sub_C 📖	mathematical	Set Set.instHasSubset U C	Real Real.instLE approx	—	approx_of_mem_C approx_nonneg approx_le_one approx_of_notMem_U
approx_le_lim 📖	mathematical	—	Real Real.instLE approx lim	—	le_ciSup bddAbove_range_approx
approx_le_one 📖	mathematical	—	Real Real.instLE approx Real.instOne	—	Set.indicator_apply_le' le_rfl zero_le_one Real.instZeroLEOneClass Nat.instAtLeastTwoHAddOfNat midpoint_eq_smul_add invOf_eq_inv add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add div_le_one PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing zero_lt_two NeZero.charZero_one IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one
approx_le_succ 📖	mathematical	—	Real Real.instLE approx	—	Real.instIsStrictOrderedRing Real.instIsOrderedAddMonoid IsStrictOrderedRing.toIsStrictOrderedModule PosSMulReflectLT.toPosSMulReflectLE Real.instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors PosSMulMono.toPosSMulReflectLT IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule approx_mem_Icc_right_left approx.eq_2 midpoint_le_midpoint
approx_mem_Icc_right_left 📖	mathematical	—	Real Set Set.instMembership Set.Icc Real.instPreorder approx right left	—	le_rfl le_imp_le_of_le_of_le le_refl Set.indicator_le_indicator_apply_of_subset Set.compl_subset_compl_of_subset left_U_subset Pi.one_apply le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one midpoint_le_midpoint Real.instIsStrictOrderedRing Real.instIsOrderedAddMonoid IsStrictOrderedRing.toIsStrictOrderedModule approx_le_approx_of_U_sub_C subset_closure
approx_mono 📖	mathematical	—	Monotone Real Nat.instPreorder Real.instPreorder approx	—	monotone_nat_of_le_succ approx_le_succ
approx_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero approx	—	Set.indicator_nonneg zero_le_one Real.instZeroLEOneClass Nat.instAtLeastTwoHAddOfNat midpoint_eq_smul_add invOf_eq_inv mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing inv_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing zero_le_two IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid add_nonneg
approx_of_mem_C 📖	mathematical	Set Set.instMembership C	approx Real Real.instZero	—	Set.indicator_of_notMem subset subset_right_C midpoint_self
approx_of_notMem_U 📖	mathematical	Set Set.instMembership U	approx Real Real.instOne	—	Set.indicator_of_mem Set.mem_compl_iff left_U_subset midpoint_self
bddAbove_range_approx 📖	mathematical	—	BddAbove Real Real.instLE Set.range approx	—	approx_le_one
closed_C 📖	mathematical	—	IsClosed C	—	—
continuous_lim 📖	mathematical	—	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace lim	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Meta.NormNum.isNNRat_lt_true Real.instIsStrictOrderedRing instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Nat.cast_one continuous_iff_continuousAt Filter.HasBasis.tendsto_right_iff Metric.nhds_basis_closedBall_pow LT.lt.trans Filter.univ_mem' pow_zero Real.dist_le_of_mem_Icc_01 lim_mem_Icc Filter.mp_mem IsOpen.mem_nhds open_U pow_succ' lim_eq_midpoint lim_of_mem_C left_U_subset_right_C LE.le.trans dist_midpoint_midpoint_le dist_self add_zero div_eq_inv_mul mul_le_mul IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedRing.toMulPosMono le_of_lt dist_nonneg div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Set.compl_subset_compl subset isOpen_compl_iff closed_C lim_of_notMem_U pow_succ le_imp_le_of_le_of_le le_refl div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid zero_add add_le_add Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isNNRat_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr
disjoint_C_support_lim 📖	mathematical	—	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice C Function.support Real Real.instZero lim	—	Function.disjoint_support_iff lim_of_mem_C
hP 📖	mathematical	IsOpen Set Set.instHasSubset	closure	—	—
left_C 📖	mathematical	—	C left	—	—
left_U_subset 📖	mathematical	—	Set Set.instHasSubset U left	—	Set.Subset.trans left_U_subset_right_C subset
left_U_subset_right_C 📖	mathematical	—	Set Set.instHasSubset U left C right	—	subset_closure
lim_eq_midpoint 📖	mathematical	—	lim midpoint Real Real.instRing invertibleTwo Semifield.toDivisionSemiring Field.toSemifield Real.instField IsStrictOrderedRing.toCharZero DivisionSemiring.toSemiring Real.partialOrder Real.instIsStrictOrderedRing Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNormedAddTorsor left right	—	tendsto_nhds_unique TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat tendsto_approx_atTop Filter.tendsto_add_atTop_iff_nat Filter.Tendsto.midpoint instIsTopologicalAddTorsor_1 ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal
lim_le_one 📖	mathematical	—	Real Real.instLE lim Real.instOne	—	ciSup_le approx_le_one
lim_mem_Icc 📖	mathematical	—	Real Set Set.instMembership Set.Icc Real.instPreorder Real.instZero Real.instOne lim	—	lim_nonneg lim_le_one
lim_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero lim	—	LE.le.trans approx_nonneg approx_le_lim
lim_of_mem_C 📖	mathematical	Set Set.instMembership C	lim Real Real.instZero	—	approx_of_mem_C ciSup_const
lim_of_notMem_U 📖	mathematical	Set Set.instMembership U	lim Real Real.instOne	—	approx_of_notMem_U ciSup_const
open_U 📖	mathematical	—	IsOpen U	—	—
right_U 📖	mathematical	—	U right	—	—
subset 📖	mathematical	—	Set Set.instHasSubset C U	—	—
subset_right_C 📖	mathematical	—	Set Set.instHasSubset C right	—	Set.Subset.trans subset left_U_subset_right_C
tendsto_approx_atTop 📖	mathematical	—	Filter.Tendsto Real approx Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace lim	—	tendsto_atTop_ciSup LinearOrder.supConvergenceClass instOrderTopologyReal approx_mono approx_le_one

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_continuousMap_one_of_isCompact_subset_isOpen 📖	mathematical	IsCompact IsOpen Set Set.instHasSubset	Set.EqOn Real DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike Pi.instOne Real.instOne tsupport Real.instZero Set.instMembership Set.Icc Real.instPreorder	—	exists_open_between_and_isCompact_closure instRegularSpaceOfWeaklyLocallyCompactSpaceOfR1Space instWeaklyLocallyCompactSpaceOfLocallyCompactSpace exists_tsupport_one_of_isOpen_isClosed isClosed_closure IsCompact.closure_subset_of_isOpen HasSubset.Subset.trans Set.instIsTransSubset subset_closure Set.EqOn.mono IsCompact.of_isClosed_subset
exists_continuous_nonneg_pos 📖	mathematical	—	HasCompactSupport Real Real.instZero DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike Pi.hasLe Real.instLE Pi.instZero	—	WeaklyLocallyCompactSpace.exists_compact_mem_nhds instWeaklyLocallyCompactSpaceOfLocallyCompactSpace exists_continuous_one_zero_of_isCompact isClosed_empty Set.disjoint_empty mem_of_mem_nhds NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing
exists_continuous_one_zero_of_isCompact 📖	mathematical	IsCompact Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	Set.EqOn Real DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike Pi.instOne Real.instOne Pi.instZero Real.instZero HasCompactSupport Set.instMembership Set.Icc Real.instPreorder	—	exists_compact_closed_between IsClosed.isOpen_compl Disjoint.subset_compl_left Disjoint.symm exists_continuous_zero_one_of_isCompact IsOpen.isClosed_compl isOpen_interior Set.disjoint_compl_right_iff_subset Set.subset_compl_comm HasSubset.Subset.trans Set.instIsTransSubset interior_subset Continuous.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal continuous_const HasCompactSupport.intro' Mathlib.Tactic.Contrapose.contrapose₂ covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid AddGroup.toOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le
exists_continuous_one_zero_of_isCompact_of_isGδ 📖	mathematical	IsCompact IsGδ Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	Set.preimage Real DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike Set.instSingletonSet Real.instOne Set.EqOn Pi.instZero Real.instZero HasCompactSupport Set.instMembership Set.Icc Real.instPreorder	—	IsGδ.eq_iInter_nat exists_compact_closed_between IsClosed.isOpen_compl Disjoint.subset_compl_left Disjoint.symm exists_continuous_one_zero_of_isCompact IsOpen.isClosed_compl IsOpen.inter isOpen_interior Set.disjoint_compl_right_iff_subset Set.subset_inter HasSubset.Subset.trans Set.instIsTransSubset Eq.subset Set.instReflSubset Set.iInter_subset Nat.instAtLeastTwoHAddOfNat div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.instAtLeastTwo pow_pos IsStrictOrderedRing.toZeroLEOneClass summable_geometric_two' tsum_geometric_two' Set.inter_subset_right interior_subset MulZeroClass.mul_zero tsum_zero mul_le_of_le_one_right IsOrderedRing.toPosMulMono LT.lt.le Summable.of_nonneg_of_le mul_nonneg continuous_tsum Real.instCompleteSpace Continuous.comp' Continuous.fun_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Continuous.fst continuous_id' Continuous.snd Continuous.prodMk continuous_const ContinuousMapClass.map_continuous ContinuousMap.instContinuousMapClass norm_mul NormedDivisionRing.toNormMulClass abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Set.Subset.antisymm mul_one Set.compl_subset_compl Set.compl_iInter lt_of_lt_of_le Summable.tsum_lt_tsum instIsTopologicalAddGroupReal OrderTopology.to_orderClosedTopology instOrderTopologyReal SummationFilter.instNeBotUnconditional SummationFilter.instLeAtTopUnconditional Eq.le LT.lt.ne Set.EqOn.mono Set.subset_compl_comm HasCompactSupport.of_support_subset_isCompact instR1Space Function.support_subset_iff' tsum_nonneg le_trans Summable.tsum_le_tsum
exists_continuous_zero_one_of_isClosed 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	Set.EqOn Real DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike Pi.instZero Real.instZero Pi.instOne Real.instOne Set.instMembership Set.Icc Real.instPreorder	—	IsClosed.isOpen_compl Set.disjoint_left normal_exists_closure_subset Urysohns.CU.continuous_lim Urysohns.CU.lim_of_mem_C Urysohns.CU.lim_of_notMem_U Urysohns.CU.lim_mem_Icc
exists_continuous_zero_one_of_isCompact 📖	mathematical	IsCompact Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	Set.EqOn Real DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike Pi.instZero Real.instZero Pi.instOne Real.instOne Set.instMembership Set.Icc Real.instPreorder	—	exists_compact_closed_between IsClosed.isOpen_compl Disjoint.subset_compl_left Disjoint.symm IsClosed.closure_subset_iff interior_subset isOpen_interior HasSubset.Subset.trans Set.instIsTransSubset IsCompact.of_isClosed_subset isClosed_closure Urysohns.CU.continuous_lim Urysohns.CU.lim_of_mem_C Urysohns.CU.lim_of_notMem_U Urysohns.CU.lim_mem_Icc
exists_continuous_zero_one_of_isCompact' 📖	mathematical	IsCompact Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	Set.EqOn Real DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike Pi.instZero Real.instZero Pi.instOne Real.instOne Set.instMembership Set.Icc Real.instPreorder	—	exists_continuous_zero_one_of_isCompact IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal sub_eq_zero_of_eq Set.EqOn.symm covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid AddGroup.toOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le
exists_tsupport_one_of_isOpen_isClosed 📖	mathematical	IsOpen IsCompact closure Set Set.instHasSubset	tsupport Real Real.instZero DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike Set.EqOn Pi.instOne Real.instOne Set.instMembership Set.Icc Real.instPreorder	—	SeparatedNhds.of_isClosed_isCompact_closure_compl_isClosed isClosed_compl_iff compl_compl HasSubset.Subset.disjoint_compl_left closure_minimal Set.subset_compl_iff_disjoint_right IsOpen.isClosed_compl HasSubset.Subset.trans Set.instIsTransSubset subset_closure isClosed_closure IsClosed.isOpen_compl Set.subset_compl_comm Set.Subset.trans IsCompact.of_isClosed_subset closure_mono Set.compl_subset_compl HasSubset.Subset.disjoint_compl_right Set.compl_subset_comm Urysohns.CU.continuous_lim IsClosed.closure_eq Disjoint.subset_compl_right Set.disjoint_of_subset_right Disjoint.symm Urysohns.CU.disjoint_C_support_lim Urysohns.CU.lim_of_notMem_U Set.notMem_compl_iff Urysohns.CU.lim_mem_Icc

---

← Back to Index