Basic

📁 Source: Mathlib/Topology/Defs/Basic.lean

Statistics

Metric	Count
Definitions BaireSpace, DenseRange, IsClopen, IsClosed, IsClosedMap, IsOpen, IsOpenMap, IsOpenQuotientMap, IsOpen, Continuous_of, IsClosed_of, IsOpen_of, closure_of, closure, coborder, frontier, interior	17
Theorems baire_property, isOpen_preimage, isOpen_compl, inter, continuous, isOpenMap, surjective, isOpen_inter, isOpen_sUnion, isOpen_univ, isOpenQuotientMap_iff, isOpen_sUnion, isOpen_univ	13
Total	30

BaireSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baire_property 📖	mathematical	IsOpen Dense	Set.iInter	—	—

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOpen_preimage 📖	mathematical	Continuous IsOpen	Set.preimage	—	—

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOpen_compl 📖	mathematical	—	IsOpen Compl.compl Set Set.instCompl	—	—

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inter 📖	mathematical	IsOpen	Set Set.instInter	—	TopologicalSpace.isOpen_inter

IsOpenQuotientMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous 📖	mathematical	IsOpenQuotientMap	Continuous	—	—
isOpenMap 📖	mathematical	IsOpenQuotientMap	IsOpenMap	—	—
surjective 📖	—	IsOpenQuotientMap	—	—	—

TopologicalSpace

Definitions

Name	Category	Theorems
IsOpen 📖	MathDef	12 math math: RingTopology.ext_iff, DiffeologicalSpace.CorePlotsOn.isOpen_iff_preimages_plots, Topology.WithLawson.isOpen_preimage_ofLawson, GroupTopology.ext'_iff, Topology.WithScott.isOpen_iff_isUpperSet_and_scottHausdorff_open', Topology.WithUpper.isOpen_preimage_ofUpper, Topology.WithLawson.isOpen_def, isOpen_fold, Topology.WithUpper.isOpen_def, isOpen_univ, AddGroupTopology.ext'_iff, DiffeologicalSpace.isOpen_iff_preimages_plots

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOpen_inter 📖	mathematical	IsOpen	Set Set.instInter	—	—
isOpen_sUnion 📖	mathematical	IsOpen	Set.sUnion	—	—
isOpen_univ 📖	mathematical	—	IsOpen Set.univ	—	—

Topology

Definitions

Name	Category	Theorems
Continuous_of 📖	CompOp	—
IsClosed_of 📖	CompOp	—
IsOpen_of 📖	CompOp	—
closure_of 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
BaireSpace 📖	CompData	9 math math: BaireSpace.of_t2Space_locallyCompactSpace, Topology.IsOpenEmbedding.baireSpace, IsOpenQuotientMap.baireSpace, Homeomorph.baireSpace, IsGδ.of_t2Space_locallyCompactSpace, baire_of_finite, IsOpen.baireSpace, IsGδ.baireSpace_of_dense, BaireSpace.of_completelyPseudoMetrizable
DenseRange 📖	MathDef	60 math math: DenseRange.zpow_of_ergodic_mul_left, AlgebraicGeometry.Scheme.Hom.denseRange, AbstractCompletion.dense, ContinuousMap.toLp_denseRange, OnePoint.denseRange_coe, PrimeSpectrum.denseRange_comap_iff_ker_le_nilRadical, PrimeSpectrum.denseRange_comap_iff_minimalPrimes, denseRange_pure, TopologicalSpace.denseRange_denseSeq, denseRange_subtype_val, NormedField.denseRange_nnnorm, ProfiniteGrp.denseRange_toLimit, AddCircle.denseRange_zsmul_iff, denseRange_smul, NormedAddCommGroup.denseRange_toCompl, ergodic_mul_left_iff_denseRange_zpow, Function.Surjective.denseRange, UniformSpace.Completion.denseRange_coe, denseRange_inclusion_iff, PowerSeries.WithPiTopology.denseRange_toPowerSeries, PadicInt.denseRange_natCast, denseRange_preStoneCechUnit, ProfiniteGrp.ProfiniteCompletion.denseRange, denseRange_zpow_iff_surjective, CauchyFilter.denseRange_pureCauchy, MeasureTheory.Lp.simpleFunc.denseRange, UniformSpace.Completion.denseRange_coe₃, AddCircle.denseRange_zsmul_coe_iff, NumberField.InfinitePlace.denseRange_algebraMap_pi, IsDenseInducing.dense, AlgebraicGeometry.isDominant_iff, Padic.denseRange_ratCast, denseRange_stoneCechUnit, denseRange_zsmul_iff_surjective, denseRange_iff_closure_range, MvPowerSeries.WithPiTopology.denseRange_toMvPowerSeries, TopologicalSpace.IsOpenCover.denseRange_iff_restrictPreimage, not_denseRange_zpow, ergodic_add_left_iff_denseRange_zsmul, Rat.denseRange_cast, Metric.denseRange_iff, LaurentSeries.coe_range_dense, denseRange_zsmul_iff_nsmul, Dense.denseRange_val, DenseRange.zsmul_of_ergodic_add_left, TopologicalSpace.exists_dense_seq, denseRange_zpow_iff_pow, UniformSpace.Completion.denseRange_coe₂, AlgebraicGeometry.IsDominant.denseRange, denseRange_discrete, EReal.denseRange_ratCast, MeasureTheory.Lp.simpleFunc.denseRange_coeSimpleFuncNonnegToLpNonneg, PadicInt.denseRange_intCast, NumberField.InfiniteAdeleRing.denseRange_algebraMap, denseRange_vadd, AlgebraicGeometry.dominant_eq_topologically, SchwartzMap.denseRange_toLpCLM, not_denseRange_zsmul, BoundedContinuousFunction.toLp_denseRange, denseRange_id
IsClopen 📖	MathDef	71 math math: PrimeSpectrum.isClopen_iff_mul_add, IsClopen.pathComponent, CompletelyRegularSpace.isTopologicalBasis_clopens_of_cardinalMk_lt_continuum, PrimeSpectrum.isClopen_iff_mul_add_zeroLocus, continuousOn_boolIndicator_iff_isClopen, isClopen_compl_iff, UniformSpace.hausdorff.isClopen_singleton_empty, TopologicalSpace.vietoris.isClopen_singleton_empty, TopologicalSpace.Compacts.isClopen_singleton_bot, Algebra.QuasiFiniteAt.isClopen_singleton, OpenAddSubgroup.isClopen, Valued.isClopen_ball, isClopen_discrete, exists_isClopen_upper_of_not_le, UniformSpace.isClopen_ball_of_isSymm_of_isTrans_of_mem_uniformity, IsValuativeTopology.isClopen_sphere, isClopen_range_inl, isClopen_univ, Valued.isClopen_valuationSubring, exists_isClopen_of_totally_separated, ClopenUpperSet.isClopen, MeromorphicOn.isClopen_setOf_meromorphicOrderAt_eq_top, IsLocallyConstant.isClopen_fiber, continuous_bool_rng, TopologicalSpace.Clopens.isClopen, PrimeSpectrum.isClopen_iff, DiscreteQuotient.isClopen_preimage, isClopen_of_disjoint_cover_open, Topology.IsQuotientMap.isClopen_preimage, isClopen_range_inr, loc_compact_Haus_tot_disc_of_zero_dim, Valued.isClopen_sphere, isTopologicalBasis_isClopen, isClopen_range_sigmaMk, UniformSpace.nhds_basis_clopens, IsValuativeTopology.isClopen_ball, isClopen_iff, Valued.isClopen_integer, IsClopen.of_cthickening_subset_self, isClopen_connectedComponent, PrimeSpectrum.isClopen_basicOpen_of_mul_add, isClopen_empty, continuous_boolIndicator_iff_isClopen, exists_clopen_of_closed_subset_open, TopologicalSpace.Clopens.isClopen', AnalyticOnNhd.isClopen_setOf_analyticOrderAt_eq_top, nhds_basis_clopen, TopologicalSpace.isTopologicalBasis_clopens, IsClopen.of_thickening_subset_self, TopologicalSpace.Closeds.isClopen_singleton_bot, isClopen_preimage_val, isClopen_iff_frontier_eq_empty, PrimeSpectrum.isClopen_iff_zeroLocus, IsUltrametricDist.isClopen_sphere, DiscreteQuotient.isClopen_setOf_rel, connectedComponent_eq_iInter_isClopen, IsUltrametricDist.isClopen_closedBall, AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt.isClopen_singleton_asFiber, exists_isClopen_upper_or_lower_of_ne, OpenSubgroup.isClopen, Profinite.Nobeling.isClosedEmbedding, PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing, totallySeparatedSpace_iff_exists_isClopen, exists_isClopen_lower_of_not_le, connectedComponent_subset_iInter_isClopen, Valued.isClopen_closedBall, CompleteType.isClopen_typesWith, PriestleySpace.priestley, IsValuativeTopology.isClopen_closedBall, compact_exists_isClopen_in_isOpen, IsUltrametricDist.isClopen_ball
IsClosed 📖	CompData	522 math math: Homeomorph.isClosed_preimage, IsExposed.isClosed, LowerSemicontinuous.isClosed_epigraph, IsClosed.relImage_of_isCompact, isClosed_univ, TopologicalSpace.Compacts.isClosed_subsets_of_isClosed, isClosed_of_mem_irreducibleComponents, Topology.lawsonClosed_of_lowerClosed, AddSubgroup.isClosed_topologicalClosure, ContinuousLinearMap.IsIdempotentElem.isClosed_range, isClosed_fixedPoints, PrimeSpectrum.vanishingIdeal_isClosed_isIrreducible, Metric.isCompact_iff_isClosed_bounded, Subsemiring.isClosed_topologicalClosure, IsLowerSet.isClosed, CompactExhaustion.isClosed, IsClosed.smul_of_ne_zero, isClosed_frontier, isClosed_iSup_iff, NormedSpace.Dual.isClosed_image_polar_of_mem_nhds, isClosed_setOf_specializes, PrimeSpectrum.isClosed_zeroLocus, ConvexCone.canLift, WeakDual.isClosed_image_polar_of_mem_nhds, OnePoint.isClosed_iff_of_notMem, IsClosed.smul₀, isClosed_sSup_iff, Submonoid.isClosed_topologicalClosure, borel_eq_generateFrom_isClosed, Subgroup.isClosed_topologicalClosure, EquicontinuousOn.isClosed_range_pi_of_uniformOnFun, IsOpen.measure_eq_iSup_isClosed, Equicontinuous.isClosed_setOf_tendsto, TopologicalSpace.Closeds.isClosed, AntilipschitzWith.isClosed_range, IsClosed.smul_left_of_isCompact, OnePoint.continuousAt_infty, NonUnitalSubsemiring.isClosed_topologicalClosure, TopologicalSpace.Compacts.isClosed_inter_nonempty_of_isClosed, uniformity_hasBasis_closed, ContinuousAlternatingMap.isClosed_range_toContinuousMultilinearMap, isClosed_setOf_lipschitzOnWith, PrimeSpectrum.isClosed_iff_zeroLocus, lowerSemicontinuous_iff_isClosed_preimage, Submodule.ClosedComplemented.exists_isClosed_isCompl, IsClosed.upperClosure, nhds_basis_closeds, frontier_subset_iff_isClosed, Topology.IsUpper.continuous_iff_Iic, OnePoint.isOpen_iff_of_mem, OpenNormalSubgroup.instIsClosedCoePathComponentOne, WeakDual.CharacterSpace.union_zero_isClosed, SeparatedNhds.isClosed_right_of_isClosed_union, mem_uniformity_isClosed, isClosed_setOf_map_add, TopologicalSpace.NonemptyCompacts.isClosed_in_closeds, ContinuousOn.preimage_isClosed_of_isClosed, instHasCountableSeparatingOnIsClosedOfIsOpen, isClosed_nonneg, exists_closed_nhds_zero_neg_eq_add_subset, ClosedIciTopology.isClosed_Ici, isClosed_setOf_tendsto_birkhoffAverage, IsClosed.lowerClosure_pi, MeasurableSet.exists_isCompact_isClosed_diff_lt, Topology.RelCWComplex.isClosedBase, Topology.IsScott.isClosed_iff_isLowerSet_and_dirSupClosed, compl_mem_codiscrete_iff, OnePoint.isClosed_infty, disjoint_nested_nhds_of_not_inseparable, isClosed_singleton_of_isLocallyClosed_singleton, NormedSpace.isClosed_polar, IsClosed.relInv, IsCompact.isCompact_isClosed_basis_nhds, IsComplete.isClosed, IsLocalRing.isClosed_singleton_closedPoint, closure_subset_iff_isClosed, IsLocallyConstant.isClosed_fiber, TopologicalSpace.NoetherianSpace.exists_finite_set_isClosed_irreducible, Topology.IsInducing.isClosed_preimage, Topology.IsLower.continuous_iff_Ici, Submodule.isClosed_topologicalClosure, EMetric.isClosed_ball_top, CompactlyCoherentSpace.isClosed_iff, PrimeSpectrum.exists_isClosed_singleton_of_isJacobsonRing, ClosedSubgroup.isClosed', isClosed_Ioc_iff, UniformSpace.isClosed_ball_of_isSymm_of_isTrans_of_mem_uniformity, Topology.lawsonClosed_iff_scottClosed_of_isLowerSet, Homeomorph.isClosed_image, CompleteType.isClosed_typesWith, UpperSemicontinuous.isClosed_preimage, StarAlgebra.elemental.isClosed, closed_nhds_basis, ZeroAtInftyContinuousMap.isClosed_range_toBCF, isClosed_iff_derivedSet_subset, Set.Subsingleton.isClosed, ContinuousLinearMap.isClosed_image_coe_closedBall, Metric.isClosed_closedBall, PrimeSpectrum.isClosed_iff_zeroLocus_radical_ideal, IsClosed.exists_closed_singleton, IsClosed.relPreimage_of_isCompact, AddAction.IsPretransitive.t1Space_iff, TopologicalSpace.vietoris.isClosed_inter_nonempty_of_isClosed, Topology.IsUpper.isClosed_lowerClosure, AlgebraicGeometry.RingedSpace.zeroLocus_isClosed, Ordinal.isClosed_iff_bsup, closure_eq_iff_isClosed, Subgroup.normalCore_isClosed, OnePoint.tendsto_nhds_infty, IsClosed.union, AddMonoidHom.isClosed_range_coe, isCompact_isClosed_basis_nhds, LowerSemicontinuousOn.isClosed_re_epigraph, PrimeSpectrum.isClosed_range_of_stableUnderSpecialization, IsNoetherianRing.isClosed_ideal, ContinuousLinearMap.isClosed_ker, isClosed_range_inl, ContinuousMap.idealOfSet_closed, Urysohns.CU.closed_C, isClosed_setOf_map_zero, Topology.RelCWComplex.closed, alexandrovDiscrete_iff_isClosed, IsOpen.exists_iUnion_isClosed, ContinuousLinearMap.isClosed_image_coe_of_bounded_of_weak_closed, isClosed_sdiff_of_codiscreteWithin, isClosed_iff_frequently, TopologicalSpace.IrreducibleCloseds.instCanLiftSetCoeAndIsIrreducibleIsClosed, PeriodPair.isClosed_lattice, Valued.isClosed_valuationSubring, Topology.IsLower.isClosed_upperClosure, OnePoint.isClosed_iff_of_mem, IsClosed.vadd_right_of_isCompact, Topology.IsLowerSet.isClosed_iff_isUpper, T1Space.t1, ProjectiveSpectrum.isClosed_zeroLocus, TopologicalSpace.IsOpenCover.isClosed_iff_coe_preimage, OnePoint.isClosed_image_coe, exists_compact_closed_between, Submodule.closed_of_finiteDimensional, Ideal.IsMaximal.isClosed, isClosed_and_discrete_iff, NumberField.InfinitePlace.Completion.isClosed_image_extensionEmbedding, ProperCone.isClosed, isClosed_le, Topology.isQuotientMap_iff_isClosed, NonUnitalSubring.isClosed_topologicalClosure, IsNowhereDense.subset_of_closed_isNowhereDense, Topology.CWComplex.closed, IsClosed.add_left_of_isCompact, AddSubgroup.isClosed_of_isOpen, MeasurableSet.exists_isClosed_lt_add, OrderClosedTopology.isClosed_le', LinearMap.isClosed_range_coe, isClosed_intrinsicClosure, Homeomorph.isClosed_setOf_iff, AlgebraicGeometry.IsClosedImmersion.iff_isPreimmersion, nonunits.isClosed, isClosed_preCantorSet, IsClosed.preimage_val, Topology.IsCoherentWith.isClosed_iff, UniformSpace.isClosed_ball_of_isSymmetricRel_of_isTransitiveRel_of_mem_uniformity, ContinuousLinearMap.closed_complemented_range_of_isCompl_of_ker_eq_bot, AddSubgroup.isClosed_of_discrete, Metric.isClosed_of_pairwise_le_dist, AddHom.isClosed_range_coe, lowerSemicontinuous_iff_isClosed_epigraph, isClosed_stdSimplex, isClosed_setOf_inseparable, isClosed_nullSubgroup, IsClosed.mono, EquicontinuousOn.isClosed_range_pi_of_uniformOnFun', ClosedAddSubgroup.isClosed', Filter.hasBasis_coclosedCompact, QuotientAddGroup.t1Space_iff, isClosed_antitoneOn, isClosed_isNowhereDense_iff_compl, EMetric.isClosed_subsets_of_isClosed, Finset.isClosed, isClosed_imp, lowerSemicontinuousOn_iff_isClosed_epigraph, AffineSubspace.closed_of_finiteDimensional, Valued.isClosed_ball, ClosedIicTopology.isClosed_Iic, IsClosed.everywherePosSubset, NonUnitalStarAlgebra.elemental.isClosed, AddSubmonoid.isClosed_topologicalClosure, isClosed_induced_iff', isClosed_setOf_map_smul, isClosed_mulTSupport, ContinuousLinearMap.isClosed_range_iff_antilipschitz_of_injective, coborder_eq_univ_iff, Valued.isClosed_sphere, IsClosed.vadd, IsValuativeTopology.isClosed_closedBall, Perfect.closed, Set.Finite.isClosed_convexHull, MeasureTheory.isClosed_aestronglyMeasurable, MeasureTheory.Measure.WeaklyRegular.innerRegular_measurable, IsClosed.mul_left_of_isCompact, exists_closed_nhds_one_inv_eq_mul_subset, EquicontinuousOn.isClosed_range_uniformOnFun_iff_pi, NumberField.InfinitePlace.Completion.isClosed_image_extensionEmbeddingOfIsReal, PrimeSpectrum.isClosed_singleton_iff_isMaximal, NonUnitalAlgebra.elemental.isClosed, MeasureTheory.Measure.InnerRegular.innerRegularWRT_isClosed_isOpen, Subgroup.isClosed_of_discrete, IsClosed.mul_right_of_isCompact, ContinuousAlgEquiv.isClosed_image, WithZeroTopology.isClosed_iff, MeasureTheory.mem_closedCompactCylinders, IsClosed.epigraph, TopCat.isClosed_iff_of_isColimit, TopologicalSpace.Closeds.isClosed_subsets_of_isClosed, not_specializes_iff_exists_closed, NormedAddGroupHom.isClosed_ker, isClosed_diagonal, IsClosed.vadd_left_of_isCompact, MeasureTheory.innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure, IsClosed.sdiff, Topology.IsClosedEmbedding.isClosed_iff_preimage_isClosed, IsClosed.leftCoset, Profinite.NobelingProof.isClosed_C0, spectrum.isClosed, isClosed_of_spaced_out, isClosed_iff_ultrafilter, isClosed_const, TopologicalSpace.NonemptyCompacts.isClosed_inter_nonempty_of_isClosed, MeasureTheory.IsClosed.cylinder, TopologicalSpace.IrreducibleCloseds.isClosed, isClosed_cantorSet, isClosed_intrinsicFrontier, t2_iff_isClosed_diagonal, MulHom.isClosed_range_coe, TopologicalSpace.IrreducibleCloseds.is_closed', continuous_iff_isClosed, Topology.RelCWComplex.isClosed_closedCell, isPiSystem_isClosed, PrimeSpectrum.isClosed_iff_zeroLocus_ideal, isClosed_empty, Subgroup.isClosed_of_isOpen, exists_subset_iUnion_closed_subset, isClosed_range_sigmaMk, CompactlyGeneratedSpace.isClosed_iff_of_t2, Topology.IsUpperSet.isClosed_iff_isLower, isClosed_setOf_clusterPt, IntermediateField.fixingSubgroup_isClosed, exists_closed_cover_approximatesLinearOn_of_hasFDerivWithinAt, SmoothBumpFunction.isClosed_image_of_isClosed, StarSubalgebra.isClosed_topologicalClosure, AlgebraicGeometry.isClosed_singleton_iff_locallyOfFiniteType, hasBasis_coclosedLindelof, Valued.isClosed_integer, SmoothBumpFunction.isClosed_symm_image_closedBall, isClosed_Iic, isClosed_induced_iff, IsClosed.hypograph, LinearMap.polar_weak_closed, WeakDual.isClosed_closedBall, IsOpen.isClosed_compl, Topology.RelCWComplex.isClosed, Submodule.isClosed_orthogonal, NumberField.InfinitePlace.Completion.isClosed_image_extensionEmbedding_of_isReal, Topology.isClosedEmbedding_iff, Subsemigroup.isClosed_topologicalClosure, isClosed_singleton_inter, CofiniteTopology.isClosed_iff, Submodule.ClosedComplemented.isClosed, TopologicalSpace.IrreducibleCloseds.equivSubtype_apply, exists_iUnion_eq_closed_subset, IsClosed.prod, perfect_def, IsTopologicalGroup.t2Space_iff_one_closed, TopologicalSpace.ext_iff_isClosed, SequentialSpace.isClosed_of_seq, isClosed_range_of_spaced_out, AlgebraicGeometry.Scheme.eq_zeroLocus_of_isClosed_of_isAffine, MeasureTheory.isClosed_setOf_preimage_ae_eq, Topology.IsScottHausdorff.isClosed_of_isUpperSet, OpenNormalAddSubgroup.instIsClosedCoePathComponentZero, mem_coclosedLindelof, isClosed_monotone, EMetric.NonemptyCompacts.isClosed_in_closeds, Topology.IsQuotientMap.isClosed_preimage, isClosed_asymptoticCone, PrimeSpectrum.stableUnderSpecialization_range_iff, WeakDual.isClosed_polar, isClosed_Icc, stableUnderSpecialization_iff_exists_sUnion_eq, IsClosed.smul_right_of_isCompact, lowerHemicontinuous_iff_isClosed_preimage_Iic, IsClopen.isClosed, isClosed_tsupport, isSeqClosed_iff_isClosed, isClosed_setOf_map_inv, isClosed_preimage_val_coborder, Topology.lawsonClosed_of_scottClosed, Subring.isClosed_topologicalClosure, MeasureTheory.innerRegularWRT_isCompact_isClosed_isOpen, isClosed_discrete, ProjectiveSpectrum.isClosed_iff_zeroLocus, Ctop.Realizer.isClosed_iff, isClosed_setOf_map_mul, isClosed_nullSubmodule, isClosed_eq, Metric.isClosed_sphere, MeasureTheory.innerRegularWRT_isCompact_closure_iff, TopologicalSpace.Clopens.isClosed, Pi.isCompact_iff, IsClosed.inv, NonUnitalSubalgebra.isClosed_topologicalClosure, ClosedSubmodule.isClosed, IsClosed.inter_preimage_val_iff, Profinite.NobelingProof.isClosed_proj, MonoidHom.isClosed_range_coe, MeasureTheory.innerRegularWRT_isCompact_isClosed_iff, isClosed_inter_singleton, IsClosed.balancedCore, isClosed_range_inr, CStarAlgebra.isClosed_nonneg, UniformSpace.isClosed_ball, discreteTopology_iff_forall_isClosed, nhds_basis_closed_balanced, Metric.isClosed_eball_top, ConvexBody.isClosed, exists_subset_iUnion_compact_subset_t2space, Profinite.NobelingProof.isClosed_C', AlgebraicGeometry.Scheme.IdealSheafData.isClosed_supportSet, TopologicalSpace.IrreducibleCloseds.isClosed', OpenAddSubgroup.isClosed, isClosed_sigma_iff, DiscreteQuotient.isClosed_preimage, upperSemicontinuous_iff_isClosed_preimage, isClosed_iff_clusterPt, isOpenMap_iff_kernImage, Topology.IsClosedEmbedding.isClosed_iff_image_isClosed, OnePoint.hasBasis_nhds_infty, MaximalSpectrum.toPrimeSpectrum_range, IsClosed.lowerClosure, Topology.WithLawson.isClosed_preimage_ofLawson, Topology.RelCWComplex.Subcomplex.closed, Subfield.isClosed_topologicalClosure, IsCompact.nhdsSet_basis_isCompact_isClosed, MeasureTheory.innerRegularWRT_isCompact_isClosed_measure_ne_top_of_group, AlgebraicGeometry.isClosed_singleton_iff_isClosedImmersion, MeasureTheory.innerRegular_isCompact_isClosed_measurableSet_of_finite, IsClosed.isClosed_le, MeasurableSet.measure_eq_iSup_isClosed_of_ne_top, IsCompact.isClosed_image_restrict, Topology.RelCWComplex.Subcomplex.closed', ClosedSubmodule.instCanLiftSubmoduleToSubmoduleIsClosedCoe, IsClosed.and, IsValuativeTopology.isClosed_ball, TopCat.partialSections.closed, Algebra.elemental.isClosed, IsGenericPoint.isClosed, Topology.lawsonClosed_iff_dirSupClosed_of_isLowerSet, PrimitiveSpectrum.isClosed_iff, LinearMap.isClosed_or_dense_ker, MeasurableSet.exists_lt_isClosed_of_ne_top, LowerSemicontinuous.isClosed_preimage, UpperHemicontinuous.isClosed_domain, Ordinal.enumOrd_isNormal_iff_isClosed, PeriodPair.isClosed_of_subset_lattice, PrimeSpectrum.comap_singleton_isClosed_of_surjective, Function.LeftInverse.isClosed_range, IsClosed.powerset_vietoris, TopologicalSpace.IrreducibleCloseds.equivSubtype'_apply, MeasureTheory.Measure.support_eq_sInter, UpperSemicontinuous.IsClosed_hypograph, MeasureTheory.closedCompactCylinders.isClosed, continuousOn_iff_isClosed, Metric.isClosed_cthickening, t2Space_iff_of_isOpenQuotientMap, isClosed_setOf_map_neg, UniformOnFun.isClosed_setOf_continuous, IsSeqClosed.isClosed, upperSemicontinuous_iff_IsClosed_hypograph, ContinuousLinearEquiv.isClosed_image, LinearMap.polar_isClosed, IsClosed.preimage, LinearMap.continuous_iff_isClosed_ker, OpenSubgroup.isClosed, Topology.IsGeneratedBy.isClosed_iff, Ordinal.isClosed_iff_iSup, IsClosed.inter, lowerSemicontinuousOn_iff_preimage_Iic, isClosed_preimage_val, Set.isClosed_centralizer, IsTopologicalAddGroup.t2Space_iff_zero_closed, MeasurableSet.isClopenable', TopologicalSpace.IrreducibleCloseds.equivSubtype_symm_apply, ModelWithCorners.isClosed_range, IsClosed.trans, specializingMap_iff_isClosed_image_closure_singleton, isClosed_Ico_iff, exists_mem_nhds_isCompact_isClosed, PrimeSpectrum.isClosed_of_stableUnderSpecialization_of_isConstructible, isClosed_sum_iff, isClosed_iff_forall_filter, MeasurableSet.exists_isCompact_isClosed_lt_add, exists_isClosed_iff, IsClosed.pathComponent, EMetric.NonemptyCompacts.isClosed_subsets_of_isClosed, Valued.isClosed_closedBall, isClosed_antitone, IsSeparatedMap.isClosed_eqLocus, UniformSpace.hausdorff.isClosed_powerset, IsClosed.relPreimage_of_finite, IsClosed.neg, ContinuousMap.isClosed_setOf_mapsTo, isClosed_connectedComponent, PrimeSpectrum.isClosed_range_comap_of_surjective, isClosed_le_of_isClosed_nonneg, isClosed_irreducibleComponent, upperHemicontinuous_iff_isClosed_compl_preimage_Iic_compl, isClosed_nullAddSubgroup, EMetric.isClosed_closedBall, Topology.IsInducing.isClosed_iff', ultrafilter_isClosed_basic, PointedCone.isClosed_dual, ULift.isClosed_iff, AddSubsemigroup.isClosed_topologicalClosure, isClosed_derivedSet, PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing, MeasureTheory.Measure.isClosed_support, EMetric.Closeds.isClosed_subsets_of_isClosed, closedAbsConvexHull_isClosed, IsClosed.powerset_hausdorff, IsClosed.isClosed_image_eval, IsClosed.add_right_of_isCompact, isClosed_closure, AlgebraicGeometry.Scheme.zeroLocus_isClosed, isClosed_iff_nhds, isClosed_omegaLimit, disjoint_nested_nhds, MeasureTheory.innerRegularWRT_isCompact_closure_of_univ, Function.locallyFinsuppWithin.closedSupport, OnePoint.isOpen_compl_image_coe, irreducibleComponents_eq_maximals_closed, isClosed_of_closure_subset, MeasureTheory.innerRegularWRT_isCompact_isClosed, IsClosed.upperClosure_pi, IsClosed.setOf_mapsTo, isClosed_singleton, upperSemicontinuousOn_iff_isClosed_hypograph, Module.isClosed_support, Submodule.closedComplemented_iff_isClosed_exists_isClosed_isCompl, Topology.RelCWComplex.isClosed_cellFrontier, WeakDual.CharacterSpace.isClosed, isClosed_induced, MeasureTheory.innerRegularWRT_isCompact, PrimeSpectrum.isClosed_comap_singleton_of_isIntegral, MeasurableSet.exists_isClosed_diff_lt, isClosed_closedAbsConvexHull, MeasureTheory.innerRegularWRT_isCompact_isClosed_measure_ne_top_of_addGroup, isClosed_monotoneOn, WeakDual.isClosed_image_coe_of_bounded_of_closed, mem_coclosed_Lindelof', Subalgebra.isClosed_topologicalClosure, IsClosed.right_addCoset, MeasureTheory.PolishSpace.innerRegular_isCompact_isClosed_measurableSet, IsClosed.left_addCoset, Set.Finite.isClosed, isClosed_setOf_lipschitzWith, Topology.IsClosedEmbedding.isClosed_range, MeasureTheory.Measure.InnerRegularWRT.of_pseudoMetrizableSpace, IsClosedMap.isClosed_range, isClosed_le_prod, InfiniteGalois.fixingSubgroup_isClosed, isClosed_Ioo_iff, isClosed_closedConvexHull, IsOpen.exists_lt_isClosed, isOpen_compl_iff, Euclidean.isClosed_closedBall, Profinite.NobelingProof.isClosed_C1, mem_closedPoints_iff, TopologicalSpace.IrreducibleCloseds.equivSubtype'_symm_apply, SeparatedNhds.isClosed_union_iff, isClosed_Ici, TopologicalSpace.Closeds.instCanLiftSetCoeIsClosed, Compactum.isClosed_iff, TopologicalSpace.Closeds.isClosed', IsClosed.isClosed_eq, IsUltrametricDist.isClosed_ball, IsCoercive.isClosed_range, PrimeSpectrum.isClosed_image_of_stableUnderSpecialization, isClosed_setOf_map_one, isSeparatedMap_iff_isClosed_diagonal, MeasureTheory.Measure.WeaklyRegular.innerRegular, isClosed_setOf_isCompactOperator, isClosed_coinduced, IsClosed.relImage_of_finite, Metric.isClosed_closedEBall, Topology.WithGeneratedByTopology.isClosed_iff, MulAction.IsPretransitive.t1Space_iff, Topology.IsInducing.isClosed_iff, TopologicalSpace.NonemptyCompacts.isClosed_subsets_of_isClosed, MeasureTheory.innerRegularWRT_isCompact_closure, IsClosed.exists_minimal_nonempty_closed_subset, AffineSubspace.isClosed_direction_iff, IsUpperSet.isClosed, Submodule.isClosed_or_dense_of_isCoatom, PrimeSpectrum.stableUnderSpecialization_image_iff, Compactum.isClosed_cl, isClosed_unitary, IsProperMap.isClosed_range, MeasureTheory.Measure.InnerRegularWRT.isCompact_isClosed, IsCompact.isClosed, IsClosed.reProdIm, upperSemicontinuousOn_iff_preimage_Ici, QuotientGroup.t1Space_iff, closedConvexHull_isClosed, UniformFun.isClosed_setOf_continuous, SeparatedNhds.isClosed_left_of_isClosed_union, Complex.isClosed_range_intCast, ClosedSubmodule.isClosed', exists_mem_nhds_isClosed_subset, IsClosed.rightCoset, CategoryTheory.PreGaloisCategory.autEmbedding_range_isClosed, isClosed_compl_iff, IsClosed.smul, NonUnitalStarSubalgebra.isClosed_topologicalClosure
IsClosedMap 📖	MathDef	85 math math: isClosedMap_prodMk_right, IsProperMap.universally_closed, isClosedMap_sigmaMk, isClosedMap_div_right, Topology.IsClosedEmbedding.isClosedEmbedding_iff_continuous_injective_isClosedMap, isClosedMap_smul_of_ne_zero, isClosedMap_inr, isClosedMap_iff_comap_nhds_le, QuotientGroup.isClosedMap_coe, IsProperMap.isClosedMap, LightProfinite.isClosedMap, isProperMap_iff_universally_closed, isClosedMap_neg, Topology.IsClosedEmbedding.isClosedMap, CompHausLike.isClosedMap, Polynomial.isClosedMap_eval, isClosedMap_iff_closure_image, isClosedMap_iff_kernImage, isClosedMap_inl, isClosedMap_iff_kernImage_interior, isClosedMap_smul, isClosedMap_restrict_of_compactSpace, AddAction.isClosedMap_quotient, isClosedMap_mul_right, IsClosedMap.of_nonempty, isClosedMap_sub_right, isClosedMap_pow, isClosedMap_ofAdd, AlgebraicGeometry.isClosedMap_isZariskiLocalAtTarget, AlgebraicGeometry.Scheme.Hom.isClosedMap, PrimeSpectrum.isClosedMap_comap_of_isIntegral, isClosedMap_vadd, isClosedMap_toDual, isClosedMap_ofMul, isSeparatedMap_iff_isClosedMap, AlgebraicGeometry.UniversallyClosed.out, isClosedMap_toAdd, isClosedMap_nndist, isClosedMap_ofDual, isProperMap_iff_isClosedMap_and_tendsto_cofinite, IsClosedMap.of_inverse, isClosedMap_iff_comap_nhdsSet_le, isProperMap_iff_isClosedMap_ultrafilter, Valued.valuation_isClosedMap, Continuous.isClosedMap, isClosedMap_add_right, isProperMap_iff_isClosedMap_of_inj, AlgebraicGeometry.isClosedMap_isStableUnderComposition, isClosedMap_sumElim, isClosedMap_swap, Topology.IsInducing.isClosedMap, IsClosed.isClosedMap_subtype_val, AlgebraicGeometry.UniversallyClosed.universally_isClosedMap, isClosedMap_iff_clusterPt, isClosedMap_mul_left, isClosedMap_prodMk_left, isProperMap_iff_isClosedMap_filter, Homeomorph.isClosedMap, isClosedMap_div_left, QuotientAddGroup.isClosedMap_coe, IsUnit.isClosedMap_smul, isClosedMap_sub_left, isClosedMap_snd_of_compactSpace, IsClosedMap.id, isProperMap_iff_isClosedMap_and_compact_fibers, isClosedMap_sum, AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsClosedMap, isHomeomorph_iff_continuous_isClosedMap_bijective, isClosedMap_toMul, isClosedMap_const, isClosedMap_fst_of_compactSpace, isClosedMap_smul₀, AlgebraicGeometry.universallyClosed_iff, TopologicalSpace.IsOpenCover.isClosedMap_iff_restrictPreimage, isClosedMap_inv, IsHomeomorph.isClosedMap, isClosedMap_smul_left, IsClosed.isClosedMap_inclusion, AlgebraicGeometry.isClosedMap_iff_specializingMap, SeparationQuotient.isClosedMap_mk, AlgebraicGeometry.universallyClosed_eq, isClosedMap_iff_upperHemicontinuous, MulAction.isClosedMap_quotient, isClosedMap_dist, isClosedMap_add_left
IsOpen 📖	MathDef	534 math math: Set.Finite.t2_separation, nhds_hasBasis_absConvex_open, subset_interior_iff_isOpen, map_nhdsWithin, Valued.isOpen_closedball, OnePoint.isOpen_def, IndiscreteTopology.isOpen_iff, Metric.isOpen_eball, Complex.isOpen_re_lt_EReal, TopologicalSpace.OpenNhdsOf.canLiftSet, TopologicalSpace.IsTopologicalBasis.isOpenMap_iff, isOpen_pi_iff, FDerivMeasurableAux.isOpen_A, isOpen_prod_iff, setOf_isOpen_iSup, Topology.IsUpper.isOpen_iff_generate_Iic_compl, exists_open_nhds_one_mul_subset, PredOrder.isOpen_iff, isOpen_lt_prod, Subgroup.isOpen_of_isClosed_of_finiteIndex, le_nhdsAdjoint_iff, discreteTopology_subtype_iff', TopCat.GlueData.open_image_open, MeasureTheory.NullMeasurableSet.exists_isOpen_symmDiff_lt, TopologicalSpace.IsTopologicalBasis.isOpen_iff, isOpen_sum_iff, isOpen_induced_eq, UniformSpace.isOpen_ball_of_mem_uniformity, TopologicalSpace.setOf_isOpen_injective, Topology.IsLowerSet.isOpen_iff_isLowerSet, Topology.IsInducing.isOpen_iff, IsUniformGroup.uniformContinuous_iff_isOpen_ker, Subgroup.isOpen_of_mem_nhds, isOpen_iff_continuous_mem, EMetric.isOpen_iff, exists_nhds_square, GroupWithZero.isOpen_singleton_zero, DiffeologicalSpace.CorePlotsOn.isOpen_iff_preimages_plots, Topology.WithLawson.isOpen_preimage_ofLawson, InfiniteGalois.isOpen_and_normal_iff_finite_and_isGalois, nhdsWithin_basis_open, MeasureTheory.Measure.isTopologicalBasis_isOpen_lt_top, Topology.IsScott.isOpen_iff_scottContinuous_mem, IsClosed.not, MeasureTheory.Measure.Regular.innerRegular, Ordinal.isOpen_singleton_iff, isLinearTopology_iff_hasBasis_open_twoSidedIdeal, Specialization.isOpen_toEquiv_preimage, OpenSubgroup.isOpen, OnePoint.isOpen_iff_of_mem, isOpen_Iio', OnePoint.isOpen_iff_of_mem', hasBasis_opens_closure, IsCompact.separation_of_notMem, Topology.IsScottHausdorff.isOpen_of_isLowerSet, isOpen_extChartAt_target, IsClosed.isOpen_compl, IsLocallyConstant.iff_exists_open, TopCat.GlueData.isOpen_iff, generateFrom_iUnion_isOpen, CompleteType.isOpen_typesWith, isOpen_lt, Subgroup.isOpen_of_one_mem_interior, separated_by_continuous, TopCat.coequalizer_isOpen_iff, Complex.isOpen_slitPlane, PrimeSpectrum.isCompact_isOpen_iff, spectrum.isOpen_resolventSet, ContinuousMap.mem_nhds_iff, isOpen_sup, CompactlyCoherentSpace.isOpen_iff, order_separated, IsLinearTopology.hasBasis_open_submodule, disjoint_nested_nhds_of_not_inseparable, OpenPartialHomeomorph.open_source, isOpen_iff_ultrafilter, OpenPartialHomeomorph.isOpen_extend_source, OnePoint.isOpen_range_coe, mem_nhds_iff, DiscreteQuotient.isOpen_setOf_rel, mem_nhds_prod_iff', SuccOrder.isOpen_singleton_of_not_isSuccPrelimit, AddSubgroup.isOpen_of_zero_mem_interior, AlgebraicGeometry.IsOpenImmersion.isOpen_range, Ordinal.isOpen_iff, IsCompact.exists_open_superset_measure_lt_top', TopologicalSpace.ext_iff, isOpen_iff_eventually, VectorBundleCore.isOpen_baseSet, isOpen_Ioo, nhdsSetWithin_basis_open, TopologicalSpace.IsTopologicalBasis.isOpen, Topology.IsQuotientMap.isOpen_preimage, isLocallyInjective_iff_isOpen_diagonal, mem_codiscrete', ContinuousMap.continuous_compactOpen, isOpen_cpolynomialAt, IsTopologicalGroup.mulInvClosureNhd.isOpen, isOpen_interior, isOpen_iff_ball_subset, Topology.IsUpperSet.isOpen_iff_isUpperSet, MeasureTheory.innerRegularWRT_isCompact_isOpen, Metric.isOpen_thickening, continuousOn_iff, not_isOpen_singleton, IsValuativeTopology.isOpen_ball, IsOpen.liftSourceTargetPropertyAt, coborder_eq_compl_frontier_iff, t1Space_iff_exists_open, AbsConvexOpenSets.coe_nhds, not_inseparable_iff_exists_open, TopologicalSpace.isOpen_top_iff, IsLowerSet.isOpen, isOpen_setOf_disjoint_nhds_nhds, inducing_sigma, FiberBundleCore.isOpen_baseSet, Topology.IsLower.isOpen_iff_generate_Ici_compl, isClosedMap_iff_kernImage, ProfiniteGrp.closedSubgroup_eq_sInf_open, TopologicalSpace.le_def, comp_open_symm_mem_uniformity_sets, lowerSemicontinuousOn_iff_preimage_Ioi, AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_open, Topology.IsOpenEmbedding.isOpen_iff_preimage_isOpen, lowerHemicontinuous_iff_isOpen_compl_preimage_Iic_compl, map_nhds, Topology.IsUpper.isTopologicalSpace_basis, Equiv.toHomeomorph_refl, nhdset_of_mem_uniformity, Valued.isOpen_sphere, AddSubgroup.isOpen_of_isClosed_of_finiteIndex, TopologicalSpace.isTopologicalBasis_opens, AlgebraicGeometry.Scheme.GlueData.isOpen_iff, isOpen_ne_fun, AddSubgroup.isOpen_of_mem_nhds, Topology.WithLowerSet.isLowerSet_toLowerSet_preimage, Disjoint.exists_open_convexes, ContinuousMap.compactOpen_eq, MeasureTheory.Content.outerMeasure_eq_iInf, Topology.isQuotientMap_iff, OpenPartialHomeomorph.isOpen_image_iff_of_subset_source, Set.exists_isOpen_lt_add, ENNReal.isOpen_ne_top, isOpen_pi_iff', IsLinearTopology.hasBasis_open_ideal, IsLocallyConstant.isOpen_fiber, isOpen_sSup_iff, QuotientAddGroup.discreteTopology_iff, prod_eq_generateFrom, Polynomial.isOpen_image_comap_of_monic, IsDiscreteValuationRing.isOpen_iff, hasBasis_nhdsSet, Euclidean.isOpen_ball, mem_nhdsSet_iff_exists, AbsConvexOpenSets.coe_isOpen, IsGδ.eq_iInter_nat, Complex.isOpen_compl_range_intCast, InfiniteGalois.isOpen_mulEquivToLimit_image_fixingSubgroup, instHasCountableSeparatingOnIsOpenOfT0SpaceOfSecondCountableTopologyElem, TopologicalSpace.generateFrom_setOf_isOpen, eventually_nhdsSet_iff_exists, FDerivMeasurableAux.isOpen_A_with_param, IsUpperSet.isOpen, separated_by_isOpenEmbedding, isOpen_compl_singleton, isOpen_singleton_nhdsAdjoint, IsCompact.exists_isOpen_closure_subset, isOpen_Iio, isClosed_isNowhereDense_iff_compl, not_specializes_iff_exists_open, Algebra.isOpen_etaleLocus, nhdsKer_subset_iff, TopologicalSpace.CompactOpens.isOpen, IsLocallyInjective.isOpen_eqLocus, exists_open_singleton_of_finite, ProjectiveSpectrum.isOpen_iff, Topology.WithUpperSet.isUpperSet_toUpperSet_preimage, forall_open_iff_discrete, TopologicalSpace.isOpen_generateFrom_of_mem, isOpen_singleton_true, IsUniformAddGroup.uniformContinuous_iff_isOpen_ker, PrimeSpectrum.isOpen_of_stableUnderGeneralization_of_isConstructible, TopologicalSpace.OpenNhdsOf.isOpen, upperSemicontinuousOn_iff_preimage_Iio, TopologicalSpace.IsTopologicalBasis.open_iff_eq_sUnion, isOpen_range_inr, Topology.WithScott.isOpen_iff_isUpperSet_and_scottHausdorff_open', isOpen_iff_forall_mem_open, isOpen_extChartAt_source, isOpen_setOf_affineIndependent, Topology.IsOpenEmbedding.isOpen_iff_image_isOpen, Algebra.quasiFiniteAt_iff_isOpen_singleton_fiber, alexandrovDiscrete_iff, MeasurableSet.exists_isOpen_diff_lt, SeparatedNhds.isOpen_union_iff, IsUltrametricDist.isOpen_sphere, Topology.WithUpper.isOpen_preimage_ofUpper, Topology.WithLower.isOpen_def, PiNat.isOpen_cylinder, exists_open_nhds_disjoint_closure, IsOpen.isImmersionAt, WithSeminorms.isOpen_iff_mem_balls, Topology.WithLawson.isOpen_def, MeasureTheory.Measure.InnerRegular.innerRegularWRT_isClosed_isOpen, PrimeSpectrum.isOpen_iff, Valued.isOpen_valuationSubring, OnePoint.isOpen_iff_of_notMem, IsCompact.measure_eq_iInf_isOpen, isOpen_iff_generate_intervals, mem_nhdsWithin, Continuous.isOpen_support, PiNat.isOpen_iff_dist, Algebra.isOpen_smoothLocus, Module.isOpen_freeLocus, Ideal.isOpen_pow_of_isMaximal, PrespectralSpace.isTopologicalBasis, disjoint_frontier_iff_isOpen, nhds_def, generateFrom_iInter, FiberPrebundle.isOpen_target_of_mem_pretrivializationAtlas_inter, ultrafilter_isOpen_basic, exists_seq_infinite_isOpen_pairwise_disjoint, IsLocalDiffeomorphAt.localInverse_open_source, QuotientGroup.discreteTopology_iff, OpenAddSubgroup.isOpen, MeasureTheory.Measure.compl_support_eq_sUnion, locallyConnectedSpace_iff_isTopologicalBasis_isOpen_isPreconnected, MeasureTheory.LocallyIntegrableOn.exists_countable_integrableOn, upperHemicontinuous_iff_isOpen_preimage_Iic, isOpen_deltaGenerated_iff, PrimeSpectrum.isOpen_basicOpen, nhdsWithin_eq, AlgebraicGeometry.isCompactOpen_iff_eq_finset_affine_union, MeasureTheory.LocallyIntegrable.integrableOn_nhds_isCompact, isOpen_univ, exists_isOpen_iff, NNReal.isOpen_Ico_zero, TopologicalSpace.Clopens.isOpen, isOpen_iSup_iff, dense_compl_singleton_iff_not_open, IsTopologicalAddGroup.addNegClosureNhd.isOpen, Topology.IsGeneratedBy.isOpen_iff, MeasurableSet.residualEq_isOpen, Set.exists_isOpen_lt_of_lt, TopologicalSpace.Opens.IsBasis.isCompact_open_iff_eq_finite_iUnion, Topology.lawsonOpen_iff_scottOpen_of_isUpperSet', DeltaGeneratedSpace.isOpen_iff, isOpen_connectedComponent, nhds_basis_opens', SuccOrder.isOpen_iff, Topology.IsOpenEmbedding.isOpen_range, eventually_nhds_iff, IsUltrametricDist.isOpen_closedBall, OpenSubgroup.isOpen', ContinuousLinearMap.isOpen_injective, locallyConnectedSpace_iff_connectedComponentIn_open, ENat.isOpen_singleton, OpenPartialHomeomorph.IsImage.isOpen_iff, Locale.PT.isOpen_iff, Filter.isOpen_setOf_mem, ContDiffWithinAt.contDiffOn', nhdsSet_eq_principal_iff, isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis, isOpen_setOf_eventually_nhds, IsLocalDiffeomorph.isOpen_range, AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens, Units.isOpen, TopologicalSpace.IsTopologicalBasis.isOpen_isPreconnected, ChartedSpace.isOpen_iff, uniformity_hasBasis_open_symmetric, Ctop.Realizer.isOpen_iff, OpenPartialHomeomorph.isOpen_symm_image_iff_of_subset_target, isOpen_Ioi, PeriodPair.isOpen_compl_lattice_diff, Metric.isOpen_ball, exists_isOpen_xor'_mem, t0Space_iff_exists_isOpen_xor'_mem, isOpen_fold, Metric.isOpen_iff, isOpen_uniformity, OrderTopology.continuous_iff, prespectralSpace_iff, AlgebraicGeometry.Scheme.Hom.isOpen_quasiFiniteAt, exists_open_convex_of_notMem, IsClopen.isOpen, Set.InjOn.exists_isOpen_superset, isOpen_gt', IsValuativeTopology.isOpen_closedBall, stabilizer_isOpen_of_isIntegral, InfiniteGalois.isOpen_iff_finite, FiberPrebundle.isOpen_source, AlgebraicGeometry.isCompactOpen_iff_eq_basicOpen_union, Pretrivialization.open_target, Complex.isOpen_im_gt_EReal, Topology.IsScottHausdorff.isOpen_iff, MeasureTheory.innerRegularWRT_isCompact_isClosed_isOpen, Subgroup.isOpen_of_openSubgroup, isOpen_singleton_of_finite_mem_nhds, TopologicalSpace.Opens.isOpen, isDiscrete_iff_forall_exists_isOpen, ContMDiffWithinAt.contMDiffOn', isOpen_coinduced, subset_interior_iff, WithZeroTopology.isOpen_iff, isLinearTopology_iff_hasBasis_open_ideal, Diffeology.isOpen_iff_preimages_plots, CompactlyCoherentSpace.isOpen_iff_forall_compactSpace, HasStrictFDerivAt.approximates_deriv_on_open_nhds, T2Space.t2, exists_open_set_nhds, TopologicalSpace.IsOpenCover.isOpen_iff_coe_preimage, PrimitiveSpectrum.isOpen_iff, UpperSemicontinuous.isOpen_preimage, TopologicalSpace.CompactOpens.isOpen', Uniform.exists_is_open_mem_uniformity_of_forall_mem_eq, exists_open_nhds_one_split, isOpen_setOf_eventually_nhdsWithin, Valued.isOpen_closedBall, nhds_def', isLocallyClosed_tfae, OpenAddSubgroup.isOpen', AddSubgroup.isOpen_of_openAddSubgroup, PredOrder.isOpen_singleton_of_not_isPredPrelimit, SmoothBumpFunction.isOpen_support, ProjectiveSpectrum.isOpen_basicOpen, Algebra.isOpen_unramifiedLocus, Valued.isOpen_ball, isOpen_ne, SuccOrder.isOpen_singleton_iff, isOpen_singleton_iff_nhds_eq_pure, nhdsKer_eq_iff_isOpen, exists_open_nhds_zero_add_subset, isOpen_discrete, MeasureTheory.LocallyIntegrableOn.exists_nat_integrableOn, Topology.WithLowerSet.isOpen_ofLowerSet_preimage, nhdsKer_def, AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_iff_isOpen_singleton_asFiber, discreteTopology_iff_forall_isOpen, TopologicalSpace.IsTopologicalBasis.continuous_iff, IsCompact.exists_open_superset_measure_lt_top, isOpen_analyticAt, interior_eq_iff_isOpen, Topology.WithGeneratedByTopology.isOpen_iff, isOpen_singleton_iff_punctured_nhds, Set.exists_isOpen_le_add, Complex.isOpen_im_lt_EReal, Topology.IsInducing.setOf_isOpen, isLinearTopology_iff_hasBasis_open_submodule, isOpen_implies_isOpen_iff, Topology.IsScott.isOpen_iff_Iic_compl_or_univ, Valued.isOpen_integer, BaireMeasurableSet.residualEq_isOpen, IsLocalRing.isOpen_maximalIdeal_pow, TopologicalSpace.gc_generateFrom, Specialization.isUpperSet_ofEquiv_preimage, isOpen_const, ContinuousLinearEquiv.isOpen, MeasureTheory.Measure.isOpen_compl_support, MeasureTheory.Measure.OuterRegular.outerRegular, isOpen_nhdsKer, isLindelof_open_iff_eq_countable_iUnion_of_isTopologicalBasis, isOpen_Iotop, LocallyConvexSpace.convex_open_basis_zero, continuousSMul_iff_stabilizer_isOpen, isGδ_iff_eq_iInter_nat, stableUnderGeneralization_iff_exists_sInter_eq, isOpen_iff_isOpen_ball_subset, OpenPartialHomeomorph.isOpen_extend_target, isOpen_isPathConnected_basis, FDerivMeasurableAux.isOpen_B_with_param, Metric.exists_isOpen_isBounded_image_of_isCompact_of_forall_continuousAt, BaireMeasurableSet.iff_residualEq_isOpen, isOpen_range_sigmaMk, isOpen_Ioi', IntermediateField.fixingSubgroup_isOpen, ChartedSpaceCore.open_source, Topology.WithLower.isOpen_preimage_ofLower, isOpen_lt', upperSemicontinuous_iff_isOpen_preimage, Set.measure_eq_iInf_isOpen, continuous_Prop, Homeomorph.isOpen_image, Complex.isOpen_setOf_mem_nhds_and_isMaxOn_norm, mem_nhdsSetWithin, generateFrom_union_isOpen, MeasurableSet.isClopenable', mem_interior, isOpen_iff_mem_nhds, InnerProductSpace.isOpen_setOf_harmonicAt, Topology.WithUpper.isOpen_def, Topology.IsScott.isOpen_iff_isUpperSet_and_dirSupInaccOn, isPiSystem_isOpen, TopologicalSpace.Opens.is_open', discreteTopology_iff_isOpen_singleton, open_dom_of_pcontinuous, PredOrder.isOpen_singleton_iff, TopCat.isOpen_iff_of_isColimit_cofork, Trivialization.open_baseSet, IsLocalHomeomorph.isTopologicalBasis, LocallyConnectedSpace.open_connected_basis, isOpen_iff_nhds, ENNReal.isOpen_Ico_zero, exists_open_nhds_zero_half, ContinuousMap.setOfIdeal_open, AnalyticOnNhd.is_constant_or_isOpen, Filter.nhds_nhds, TopCat.isOpen_iff_of_isColimit, isOpen_prod_iff', MeasureTheory.Measure.exists_isOpen_everywherePosSubset_eq_diff, IsLocallyConstant.exists_open, ShrinkingLemma.PartialRefinement.isOpen, continuousOn_iff', isOpen_inter_eq_singleton_of_mem_discrete, IsLocallyClosed.isOpen_coborder, AbsConvexOpenSets.coe_zero_mem, TopCat.colimit_isOpen_iff, AbsConvexOpenSets.coe_convex, IsDedekindDomain.isOpen_of_ne_bot, nhdsKer_subset_iff_isOpen, Metric.exists_isOpen_isBounded_image_inter_of_isCompact_of_continuousOn, locallyConnectedSpace_iff_subsets_isOpen_isConnected, exists_open_set_nhds', ContinuousMap.nhds_compactOpen, nhds_basis_opens, TopologicalSpace.NoetherianSpace.exists_isOpen_nonempty_subset_irreducibleComponent, LowerSemicontinuous.isOpen_preimage, ChartedSpaceCore.open_target, WithZeroTopology.isOpen_Iio, Topology.IsLower.isTopologicalSpace_basis, TopologicalSpace.isOpen_of_mem_countableBasis, AlgebraicGeometry.Polynomial.isOpen_imageOfDf, PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing, isOpen_iff_forall_specializes, setOf_isOpen_sSup, FDerivMeasurableAux.isOpen_B, PartialDiffeomorph.open_target, discreteTopology_iff_isOpen_singleton_zero, OpenPartialHomeomorph.open_target, stabilizer_isOpen, gaugeSeminormFamily_ball, EMetric.isOpen_ball, isOpen_iff_ultrafilter', lowerSemicontinuous_iff_isOpen_preimage, AddAction.IsPretransitive.discreteTopology_iff, Topology.lawsonOpen_iff_scottOpen_of_isUpperSet, disjoint_nested_nhds, MeasurableSet.exists_isOpen_symmDiff_lt, OnePoint.isOpen_compl_image_coe, MulAction.IsPretransitive.discreteTopology_iff, PartialDiffeomorph.open_source, IsOpenMap.isOpen_range, isOpen_sigma_iff, Topology.IsScott.isOpen_iff_isUpperSet_and_scottHausdorff_open, Urysohns.CU.open_U, ChartedSpaceCore.open_source', Filter.isOpen_iff, TopologicalSpace.NoetherianSpace.exists_open_ne_empty_le_irreducibleComponent, isOpen_sigma_fst_preimage, continuous_def, IsLocallyConstant.iff_isOpen_fiber, isAdic_iff, IsCompact.exists_isOpen_lt_of_lt, Filter.isOpen_Iic_principal, IsLocallyClosed.isOpen_preimage_val_closure, Topology.isOpenEmbedding_iff, MeasureTheory.Measure.exists_isOpen_measure_lt_top, IsCompact.exists_isOpen_lt_add, DiscreteQuotient.isOpen_preimage, IsOpen.isImmersionAtOfComplement, mem_residual_iff, MeasureTheory.LocallyIntegrable.exists_nat_integrableOn, Metric.exists_isOpen_isBounded_image_inter_of_isCompact_of_forall_continuousWithinAt, continuous_generateFrom_iff, mem_nhdsSet, isOpen_range_inl, generateFrom_inter, exists_isOpen_superset_and_isCompact_closure, Pretrivialization.open_baseSet, MeasureTheory.Measure.InnerRegularWRT.of_pseudoMetrizableSpace, isOpen_empty, AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_basicOpen, IsCompactOpenCovered.id_iff_isOpen_and_isCompact, IsValuativeTopology.isOpen_sphere, r1_separation, IsLocalRing.isOpen_iff_finite_quotient, TopologicalSpace.leftInverse_generateFrom, PrimeSpectrum.isCompact_isOpen_iff_ideal, uniformity_hasBasis_open, isLocallyClosed_iff_isOpen_coborder, IsLocallyConstant.iff_isOpen_fiber_apply, discreteTopology_iff_isOpen_singleton_one, TopologicalSpace.exists_open_prod_subset_of_mem_nhds_diagonal, CofiniteTopology.isOpen_iff, CofiniteTopology.isOpen_iff', isOpen_compl_iff, Complex.isOpen_re_gt_EReal, ULift.isOpen_iff, isOpen_induced_iff, UpperHalfPlane.isOpen_upperHalfPlaneSet, locallyConnectedSpace_iff_hasBasis_isOpen_isConnected, Ctop.Realizer.isOpen, Homeomorph.isOpen_preimage, singletons_open_iff_discrete, isOpen_setOf_linearIndependent, locPathConnectedSpace_iff_isOpen_pathComponentIn, TopologicalSpace.IsOpenCover.isOpen_iff_inter, Metric.isOpen_singleton_iff, AlgebraicGeometry.Scheme.Hom.isOpen_smoothLocus, isOpen_mk, Metric.Sigma.isOpen_iff, exists_isOpen_mem_isCompact_closure, t2_separation, isOpen_setOf_nat_le_rank, IsLinearTopology.hasBasis_open_twoSidedIdeal, MeasureTheory.Measure.WeaklyRegular.innerRegular, Continuous.isOpen_mulSupport, FiberBundleCore.open_source', IsDedekindDomain.isOpen_iff, TopologicalSpace.le_generateFrom_iff_subset_isOpen, IsLocalRing.isOpen_maximalIdeal, TopologicalSpace.Opens.IsBasis.le_iff, TopologicalSpace.Opens.instCanLiftSetCoeIsOpen, DiffeologicalSpace.isOpen_iff_preimages_plots, Topology.WithUpperSet.isOpen_ofUpperSet_preimage, Topology.IsCoherentWith.isOpen_iff, IsOpen.pathComponent, OnePoint.isOpen_image_coe, IsLinearTopology.hasBasis_open_subbimodule, Ideal.isOpen_of_isMaximal, continuous_discrete_rng, t2Space_iff, AbsConvexOpenSets.coe_balanced, isClosed_compl_iff, setOf_isOpen_sup
IsOpenMap 📖	MathDef	128 math math: Topology.IsInducing.isOpenMap, isOpenMap_neg, IsLocalDiffeomorph.isOpenMap, TopologicalSpace.IsTopologicalBasis.isOpenMap_iff, PrimeSpectrum.isOpenMap_comap_of_hasGoingDown_of_finitePresentation, isOpenMap_quotient_mk'_add, Complex.isOpenMap_im, AlgebraicGeometry.Polynomial.isOpenMap_comap_C, MvPolynomial.isOpenMap_comap_C, AlgebraicGeometry.Scheme.Cover.isOpenMap_fromGlued, isOpenMap_eval, isOpenMap_add_left, isOpenMap_iff_lowerHemicontinuous, isOpenMap_iff_nhds_le, Topology.IsOpenEmbedding.isOpenMap, isOpenMap_iff_clusterPt_comap, ContinuousLinearEquiv.isOpenMap, AlgebraicGeometry.UniversallyOpen.out, AlgebraicGeometry.isOpenMap_isZariskiLocalAtTarget, isOpenMap_sigma_map, OnePoint.isOpenMap_coe, QuotientAddGroup.isOpenMap_coe, IsTopologicalGroup.isOpenMap_iff_nhds_one, TopologicalSpace.IsOpenCover.isOpenMap_iff_comp, isOpenMap_iff_image_interior, PrimeSpectrum.isOpenMap_comap_algebraMap_tensorProduct_of_field, isOpenMap_div_right, isOpenMap_toWeakSpace_symm, Topology.IsOpenEmbedding.isOpenMap_iff, FiberBundle.isOpenMap_proj, Homeomorph.comp_isOpenMap_iff, isOpenMap_vadd, IsOpenMap.of_sections, VectorBundleCore.isOpenMap_proj, ContinuousAlgEquiv.isOpenMap, isOpenMap_add_right, IsOpenMap.of_isEmpty, Topology.isOpenEmbedding_iff_isEmbedding_isOpenMap, QuotientRing.isOpenMap_coe, isLocallyInjective_iff_isOpenMap, IsModuleTopology.isOpenMap_of_surjective, AnalyticOnNhd.is_constant_or_isOpenMap, Polynomial.isOpenMap_comap_C, isOpenMap_prod_of_discrete_right, MonoidHom.isOpenMap_of_sigmaCompact, isOpenMap_quotient_mk'_mul, IsTopologicalAddGroup.isOpenMap_iff_nhds_zero, AddMonoidHom.isOpenMap_of_sigmaCompact, AlgebraicGeometry.AffineSpace.isOpenMap_over, isOpenMap_toAdd, AlgebraicGeometry.Scheme.Hom.isOpenMap, isOpenMap_mul_right, PiLp.isOpenMap_apply, IsOpenMap.of_inverse, IsHomeomorph.isOpenMap, isOpenMap_sub_left, SeparationQuotient.isOpenMap_mk, isOpenMap_smul₀, AlgebraicGeometry.UniversallyOpen.instIsStableUnderCompositionSchemeTopologicallyIsOpenMap, AffineMap.isOpenMap_linear_iff, isOpenMap_iff_closure_kernImage, isOpenMap_fst, Submodule.isOpenMap_mkQ, TopologicalGroup.isOpenMap_iff_nhds_one, FiberBundleCore.isOpenMap_proj, AlgebraicGeometry.isOpenMap_of_generalizingMap, Topology.isOpenEmbedding_iff_continuous_injective_isOpenMap, isOpenMap_vadd_of_sigmaCompact, IsCoveringMap.isOpenMap, isOpenMap_sub_right, isOpenQuotientMap_iff, AlgebraicGeometry.UniversallyOpen.eq, isOpenMap_mul_left, AlgebraicGeometry.UniversallyOpen.universally_isOpenMap, AlgebraicGeometry.universallyOpen_iff, isOpenMap_sum, isOpenMap_inl, Homeomorph.comp_isOpenMap_iff', isOpenMap_ofMul, AffineMap.homothety_isOpenMap, QuotientGroup.isOpenMap_coe, isOpenMap_smul, isOpenMap_inv, isOpenMap_iff_kernImage, IsModuleTopology.isOpenMap_of_surjectiveₛₗ, isOpenMap_ofDual, isOpenMap_snd, isOpenMap_sigmaMk, isOpenMap_div_left, Equiv.continuous_symm_iff, TopCat.GlueData.fromOpenSubsetsGlue_isOpenMap, IsOpenMap.id, IsOpen.isOpenMap_inclusion, isOpenMap_sumElim, isOpenMap_iff_interior, isOpenMap_barycentric_coord, isOpenMap_ofAdd, ContinuousLinearMap.isOpenMap, IsHomeomorphicTrivialFiberBundle.isOpenMap_proj, LinearMap.isOpenMap_of_finiteDimensional, IsLocalHomeomorph.isOpenMap, isOpenMap_of_hasStrictDerivAt, IsOpenMap.of_nhds_le, isOpenMap_sigma, isOpenMap_smul_of_sigmaCompact, IsOpenQuotientMap.iff_isOpenMap_isQuotientMap, Equiv.isOpenMap_symm_iff, isOpenMap_prod_of_discrete_left, TopologicalGroup.isOpenMap_iff_nhds_zero, isOpenMap_of_hasStrictFDerivAt_equiv, isOpenMap_inr, IsOpenQuotientMap.isOpenMap, IsOpen.isOpenMap_subtype_val, Complex.isOpenMap_exp, ContinuousLinearMap.isOpenMap_of_ne_zero, AlgebraicGeometry.instIsZariskiLocalAtSourceTopologicallyIsOpenMap, ContinuousOpenMap.map_open', Complex.isOpenMap_re, Units.isOpenMap_val, AlgebraicGeometry.Scheme.Cover.fromGlued_open_map, AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsOpenMap, IsUnit.isOpenMap_smul, Homeomorph.isOpenMap, AffineMap.isOpenMap, isOpenMap_toDual, TopologicalSpace.IsOpenCover.isOpenMap_iff_restrictPreimage, isOpenMap_toMul, ContinuousOpenMapClass.map_open
IsOpenQuotientMap 📖	CompData	23 math math: QuotientAddGroup.isOpenQuotientMap_mk, Topology.IsInducing.isOpenQuotientMap_of_surjective, Submodule.isOpenQuotientMap_mkQ, IsQuotientCoveringMap.isOpenQuotientMap, AddAction.isOpenQuotientMap_quotientMk, IsOpenQuotientMap.id, IsModuleTopology.isOpenQuotientMap_of_surjective, Complex.isOpenQuotientMap_pow, MonoidHom.isOpenQuotientMap_of_isQuotientMap, MulAction.isOpenQuotientMap_quotientMk, Complex.isOpenQuotientMap_zpow_compl_zero, isOpenQuotientMap_iff, SeparationQuotient.isOpenQuotientMap_mk, Polynomial.isOpenQuotientMap_eval, Polynomial.C_eq_or_isOpenQuotientMap_eval, IsOpenQuotientMap.of_isOpenMap_isQuotientMap, IsAddQuotientCoveringMap.isOpenQuotientMap, Complex.isOpenQuotientMap_pow_compl_zero, QuotientGroup.isOpenQuotientMap_mk, IsOpenQuotientMap.iff_isOpenMap_isQuotientMap, QuotientRing.isOpenQuotientMap_mk, Homeomorph.isOpenQuotientMap, AddMonoidHom.isOpenQuotientMap_of_isQuotientMap
closure 📖	CompOp	678 math math: mem_closure_iff_nhds_zero, PrimeSpectrum.closure_range_comap, closure_nonempty_iff, closure_diff_intrinsicFrontier, UniformSpace.closure_subset_image, IsClosedMap.closure_image_subset, closure_Icc, ExtremallyDisconnected.open_closure, mem_closure_iff, mapClusterPt_atTop_pow_tfae, OpenPartialHomeomorph.IsImage.closure, Metric.cthickening_closure, EquicontinuousAt.closure', closure_interior_Icc, IsOpen.div_closure, isGenericPoint_closure, Equicontinuous.closure', ContinuousLinearEquiv.image_closure, Finset.closure_biUnion, IsIrreducible.genericPoint_closure_eq, subset_closure_inter_of_isPreirreducible_of_isOpen, Complex.exists_mem_frontier_isMaxOn_norm, Metric.hausdorffEDist_closure, thickenedIndicatorAux_tendsto_indicator_closure, set_smul_closure_subset, Set.UniformEquicontinuousOn.closure, frontier_union_subset, Submonoid.top_closure_mul_self_subset, JacobsonSpace.closure_inter_closedPoints, ProjectiveSpectrum.vanishingIdeal_closure, closure_lt_subset_le, Continuous.range_subset_closure_image_dense, closure_eq_cluster_pts, closure_one_eq, isCompact_closure_interUnionBalls, MeasureTheory.Measure.haarMeasure_closure_self, group_inseparable_iff, closure_thickening, TopologicalSpace.vietoris.specializes_closure, SeparatedNhds.disjoint_closure_left, tangentConeAt_eq_biInter_closure, Subalgebra.topologicalClosure_coe, IsGenericPoint.def, mem_closure_of_frequently_of_tendsto, Complex.closure_preimage_im, ClosedSubmodule.coe_sSup, QuotientAddGroup.norm_mk_eq_zero_iff_mem_closure, dense_closure, Dynamics.coverEntropyInf_closure, Metric.diam_closure, mem_closure_iff_nhds, coborder_inter_closure, ConvexCone.coe_closure, exists_subset_iUnion_closure_subset, Subtype.dense_iff, Set.MapsTo.closure_left, NumberField.mixedEmbedding.fundamentalCone.compactSet_eq_union_aux₁, hasBasis_opens_closure, Submodule.closure_subset_topologicalClosure_span, exists_subset_iUnion_closure_subset_t2space, bddBelow_closure, IsCompact.measure_closure, Ioo_subset_closure_interior, IsOpen.closure_inter, BddBelow.closure, Subsemigroup.top_closure_mul_self_subset, IsOpen.add_closure, mem_closure_iff_frequently, Topology.IsLowerSet.closure_eq_upperClosure, EMetric.infEdist_pos_iff_notMem_closure, subset_closure_inter_union_closure_compl_left, IsDenseEmbedding.subtypeEmb_coe, LocallyFinite.closure_iUnion, mapsTo_gaugeRescale_closure, isNowhereDense_iff_forall_notMem_nhds, closure_iUnion₂_lt_nat, IsOpen.mul_closure_one_eq, MeasureTheory.Measure.haar.addHaarContent_outerMeasure_closure_pos, T25Space.t2_5, R0Space.closure_singleton, MeasureTheory.Measure.addHaarMeasure_closure_self, iUnion_closure_compactCovering, indicator_thickening_eventually_eq_indicator_closure, closure_subset_iff_isClosed, Metric.hausdorffEDist_closure_right, closure_inter_of_codisjoint_interior, Filter.HasBasis.lift'_closure_eq_self, Perfect.closure_nhds_inter, QuotientGroup.norm_mk_eq_zero_iff_mem_closure, IsIrreducible.isGenericPoint_genericPoint_closure, closure_le_eq, set_vadd_closure_subset, subset_closure, closure_minimal, Metric.hausdorffEDist_self_closure, uniqueDiffWithinAt_closure, isEmbedding_sumElim, closure_Iio', Convex.closure_subset_interior_image_homothety_of_one_lt, closedConvexHull_eq_closure_convexHull, omegaLimit_def, closure_uIoo, preperfect_iff_perfect_closure, Specializes.mem_closure, Metric.mem_closure_iff_infDist_zero, Metric.hausdorffDist_self_closure, isCompactOperator_iff_isCompact_closure_image_ball, NumberField.mixedEmbedding.fundamentalCone.volume_interior_eq_volume_closure, closure_iUnion, UniformSpace.hausdorff.uniformContinuous_closure, Topology.IsScott.lowerClosure_subset_closure, closure_smul₀, Convex.combo_interior_closure_subset_interior, HasUpperLowerClosure.isLowerSet_closure, hasCompactMulSupport_def, ite_inter_closure_compl_eq_of_inter_frontier_eq, closure_smul₀', UniformSpace.hausdorff.nhds_closure, Metric.ediam_closure, IsOpenMap.preimage_closure_eq_closure_preimage, Metric.hausdorffDist_zero_iff_closure_eq_closure, mapClusterPt_atTop_nsmul_tfae, Ordinal.mem_closure_iff_bsup, Homeomorph.image_closure, thickenedIndicatorAux_closure_eq, Metric.closure_closedBall, Filter.mem_coclosedCompact_iff, specializingMap_iff_closure_singleton_subset, EMetric.mem_closure_iff_infEdist_zero, frontier_prod_eq, SpecializingMap.closure_singleton_subset, UniformEquicontinuousOn.closure', closure_eq_iff_isClosed, mem_closure_one_iff_norm, exists_iUnion_eq_closure_subset, IsLowerSet.closure, measurableSet_closure, Metric.isBounded_closure_of_isBounded, Metric.IsCover.isCompact_closure, ContinuousWithinAt.image_closure, uniformity_eq_uniformity_closure, Pi.isCompact_closure_iff, mem_closure_iff_nhds', Metric.closure_sphere, isClosedMap_iff_closure_image, Dynamics.coverMincard_closure_le, Filter.HasBasis.hasBasis_of_isDenseInducing, mem_closure_iff_comap_neBot, Complex.closure_setOf_lt_im, genericPoints.closure, Subsemigroup.coe_topologicalClosure, closure_empty_iff, closure_inter_coborder, AbstractCompletion.closure_range, EMetric.infEdist_closure_pos_iff_notMem_closure, Set.MapsTo.closure, disjoint_nhdsSet_principal, Compactum.cl_eq_closure, IsNowhereDense.closure, diff_subset_closure_iff, exists_homeomorph_image_interior_closure_frontier_eq_unitBall, uniformity_hasBasis_closure, EMetric.countable_closure_of_compact, Filter.lift'_closure_eq_bot, IsGLB.mem_closure, specializes_iff_mem_closure, closure_uIoc, Convex.toWeakSpace_closure, closure_eq_uniformity, IsGenericPoint.image, IsDenseInducing.closure_range, StableUnderSpecialization.Union_eq, jacobsonSpace_iff, Set.Finite.closure_biUnion, IsClosed.closure_eq, ContinuousLinearMap.eqOn_closure_span, one_mem_posTangentConeAt_iff_mem_closure, TopologicalSpace.IsTopologicalBasis.exists_closure_subset, extDerivWithin_extDerivWithin_eqOn, BoundedContinuousFunction.arzela_ascoli, closure_image_closure, tendsto_measure_cthickening, clusterPt_iff_lift'_closure', LocallyFinite.closure, exists_open_between_and_isCompact_closure, Filter.mem_closure, Topology.IsLowerSet.closure_singleton, Set.Finite.isCompact_closure, isInducing_sumElim, closure_subtype, SeparationQuotient.image_mk_closure, subsingleton_image_closure_of_finite_of_isPreirreducible, mem_closure_ne_iff_frequently_within, Submodule.mapsTo_smul_closure, Set.EqOn.closure, closure_inter_subset, Metric.infDist_closure, IsOpen.inter_closure, IsOpen.closure_div, Metric.cthickening_zero, IsCompact.closure, dense_iff_closure_eq, lift'_nhds_closure, IsClosed.mem_iff_closure_subset, gauge_closure_zero, closure_ball_subset, asymptoticCone_affineSubspace, TopologicalSpace.IsSeparable.closure, Topology.IsInducing.disjoint_of_sumElim_aux, Ioc_subset_closure_interior, uniqueDiffWithinAt_iff, MeasureTheory.Measure.MeasureDense.indicatorConstLp_subset_closure, IsCompact.exists_isOpen_closure_subset, UniformSpace.subset_countable_closure_of_almost_dense_set, Preperfect.perfect_closure, closure_inter_subset_inter_closure, closure_upperClosure_comm_pi, IsCompact.closure_eq_biUnion_inseparable, Convex.interior_closure_eq_interior_of_nonempty_interior, AddSubgroup.coe_topologicalClosure_bot, AddSubmonoid.top_closure_add_self_subset, denseRange_inclusion_iff, exists_nhds_disjoint_closure, IsOpen.closure_add, closure_openSegment, closure_of_rat_image_lt, isNowhereDense_iff_disjoint, mem_closure_zero_iff_norm, ContinuousAlgEquiv.image_closure, Metric.closure_eq_iInter_cthickening, closedConvexHull_closure_eq_closedConvexHull, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_closure_subset_compactSet, tendsto_measure_thickening, closure_mono, interior_closure_idem, DenseRange.subset_closure_image_preimage_of_isOpen, StarSubalgebra.topologicalClosure_coe, closure_convexHull_extremePoints, IsOpen.sub_closure, UniformSpace.hausdorff.isUniformInducing_closure, Metric.mem_closure_iff, closure_union, totallyBounded_closure, EMetric.diam_closure, Bornology.IsBounded.isCompact_closure, Bornology.relativelyCompact.isBounded_iff, Complex.eqOn_closure_of_isPreconnected_of_isMaxOn_norm, exists_open_nhds_disjoint_closure, mem_closure_iff_nhds_basis', Metric.mem_closure_iff_infEDist_zero, Topology.IsUpperSet.closure_eq_lowerClosure, ContinuousMap.AlgHom.closure_ker_inter, NumberField.mixedEmbedding.fundamentalCone.closure_normLeOne_subset, mem_closure_iff_clusterPt, LinearMap.image_closure_of_convex, coborder_eq_union_closure_compl, tangentConeAt_closure, Set.MapsTo.closure_of_continuousWithinAt, Metric.cthickening_eq_biUnion_closedBall, Convex.closure_interior_eq_closure_of_nonempty_interior, closure_open_halfSpace, LinearEquiv.image_closure_of_convex, image_subset_closure_compl_image_compl_of_isOpen, TopologicalSpace.IsTopologicalBasis.nhds_basis_closure, isPreirreducible_iff_closure, IsPreconnected.closure, closure_addSubmonoidClosure_eq_closure_addSubgroupClosure, ContinuousAlgHom.eqOn_closure_adjoin, Balanced.closure, Dense.closure_eq, Subgroup.topologicalClosure_coe, mem_closure_iff_nhdsWithin_neBot, Convex.closure, isCompact_closure_singleton, inseparable_iff_mem_closure, MeasureTheory.innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure, mem_closure_iff_nhds_one, closure_eq_self_union_derivedSet, IsLUB.mem_closure, EMetric.subset_countable_closure_of_almost_dense_set, Complex.closure_preimage_re, PointedCone.coe_closure, closure_Ici, isGenericPoint_def, TopologicalSpace.IsTopologicalBasis.mem_closure_iff, ContinuousMap.sublattice_closure_eq_top, Metric.closure_thickening_subset_cthickening, isUniformEmbedding_subtypeEmb, Metric.infEDist_closure_pos_iff_notMem_closure, IsConnected.closure, mem_closure_pi, IsOpen.closure_sub, frontier_closure_subset, Dense.open_subset_closure_inter, IsOpen.add_closure_zero_eq, closure.mono, PrimeSpectrum.le_iff_mem_closure, Valued.closure_coe_completion_v_lt, IsClosed.mul_closure_one_eq, smul_closure_orbit_subset, sInf_mem_closure, MeasureTheory.measure_le_measure_closure_of_levyProkhorovEDist_eq_zero, Convex.combo_closure_interior_subset_interior, NormedSpace.polar_closure, Valued.closure_coe_completion_v_mul_v_lt, MeasurableSet.add_closure_zero_eq, thickenedIndicator_tendsto_indicator_closure, Metric.mem_closure_range_iff, Ordinal.mem_closure_iff_iSup, Urysohns.CU.hP, Submodule.closure_coe_iSup_map_single, Set.Subsingleton.closure_eq, closure_Iio, hasFDerivWithinAt_closure_of_tendsto_fderiv, tendsto_lift'_closure_nhds, Metric.closedBall_zero', Submodule.smul_closure_subset, vadd_set_closure_subset, Metric.closure_ball_subset_closedBall, closure_zero_eq, intrinsicClosure_eq_closure_inter_affineSpan, IsClosed.closure_subset_iff, omegaLimit_eq_biInter_inter, Topology.IsUpper.closure_singleton, mem_closure_iff_seq_limit, Disjoint.closure_right, Ordinal.mem_closure_tfae, Convex.set_average_mem_closure, IsIrreducible.closure, Dynamics.IsDynCoverOf.closure, closure_singleton, isCompactOperator_iff_exists_mem_nhds_isCompact_closure_image, SeparatedNhds.disjoint_closure_right, forall_isClosed_iff, IsCompact.closure_eq_biUnion_closure_singleton, genericPoint_closure, isOpenMap_iff_closure_kernImage, closure_Iic, Metric.hausdorffEDist_zero_iff_closure_eq_closure, Metric.closure_subset_cthickening, NumberField.mixedEmbedding.fundamentalCone.closure_paramSet, closure_residualEq, ClosedSubmodule.mem_sup, ClosedSubmodule.mem_iSup, SeminormedAddCommGroup.mem_closure_iff, DenseRange.closure_range, IsCompact.mul_closure_one_eq_closure, UniformEquicontinuous.closure', Complex.closure_setOf_re_lt, EMetric.infEdist_closure, clusterPt_lift'_closure_iff, AbsConvex.closure, hasCompactSupport_def, AddSubsemigroup.coe_topologicalClosure, IsOpen.subset_interior_closure, Complex.norm_eqOn_closure_of_isPreconnected_of_isMaxOn, Set.Nonempty.closure, Set.Equicontinuous.closure, closure_closedPoints, exists_homeomorph_image_eq, vadd_closure_subset, PrimeSpectrum.closure_image_comap_zeroLocus, AddSubmonoid.top_closure_add_self_eq, disjoint_nhds_nhdsSet, IsDenseInducing.closure_image_mem_nhds, IsClosedMap.lift'_closure_map_eq, MeasureTheory.measure_add_closure_zero, Submodule.topologicalClosure_coe, IsCompact.closure_subset_measurableSet, TopologicalSpace.IsSeparable.exists_countable_dense_subset, range_deriv_subset_closure_span_image, PrimeSpectrum.closure_singleton, NormedAddGroupHom.ker_completion, BddAbove.closure, subsingleton_closure, Filter.HasBasis.uniformity_closure, Metric.isCompact_closure_iff_exists_finite_isCover, ClusterPt.mem_closure, closure_submonoidClosure_eq_closure_subgroupClosure, mem_closure_iff_ultrafilter, IsCompact.add_closure_zero_eq_closure, Filter.closure_singleton, isCompactOperator_iff_isCompact_closure_image_closedBall, Complex.closure_setOf_lt_re, Metric.hausdorffEDist_closure_left, closure_eq_self_union_frontier, IsCompact.closure_subset_of_isOpen, ProjectiveSpectrum.zeroLocus_vanishingIdeal_eq_closure, indicator_cthickening_eventually_eq_indicator_closure, MeasureTheory.innerRegularWRT_isCompact_closure_iff, SeparationQuotient.preimage_mk_closure, Complex.closure_reProdIm, Metric.isBounded_closure_iff, ContinuousWithinAt.eqOn_const_closure, seqClosure_eq_closure, Set.Finite.closure_sUnion, smul_set_closure_subset, Filter.Tendsto.lift'_closure, EMetric.hausdorffEdist_zero_iff_closure_eq_closure, ShrinkingLemma.PartialRefinement.closure_subset, closure_iUnion_of_finite, DiffContOnCl.continuousOn, subset_mul_closure_one, IsDenseEmbedding.subtype, Subgroup.coe_topologicalClosure_bot, Metric.hausdorffDist_closure₂, Metric.hausdorffDist_closure, denseRange_iff_closure_range, Filter.compl_mem_coclosedCompact, asymptoticCone_closure, ClosedSubmodule.mem_sSup, notMem_closure_iff_nhdsWithin_eq_bot, clusterPt_iff_forall_mem_closure, JacobsonSpace.closure_inter_closedPoints_eq_closure, isLocallyClosed_tfae, closure_ordConnected_inter_rat, TopologicalSpace.Closeds.coe_sSup, IsClosed.closure_subset, TopologicalSpace.isSeparable_closure, subset_add_closure_zero, Homeomorph.preimage_closure, Dynamics.coverEntropy_closure, closure_pi_set, UniformSpace.mem_closure_iff_ball, ModelWithCorners.range_eq_closure_interior, ModelWithCorners.range_subset_closure_interior, Metric.closure_eq_iInter_thickening', disjoint_principal_nhdsSet, closure_Ioi', Filter.HasBasis.biInter_biUnion_ball, ArzelaAscoli.isCompact_closure_of_isClosedEmbedding, image_gaugeRescaleHomeomorph_closure, closure_compl, IsClosed.closure_interior_subset, Ico_subset_closure_interior, MeasurableSet.mul_closure_one_eq, Subsemiring.topologicalClosure_coe, exists_isCompact_superset_iff, UniformSpace.hausdorff.continuous_closure, OpenPartialHomeomorph.preimage_closure, Metric.mem_closure_range_iff_nat, IsCompact.closure_eq_nhdsKer, frontier_eq_closure_inter_closure, eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset, closure_closure, EquicontinuousOn.closure', Ideal.coe_closure, tendsto_mulIndicator_thickening_mulIndicator_closure, Metric.infEDist_closure, PointedCone.mem_closure, Topology.IsClosedEmbedding.closure_image_eq, hasBasis_nhds_closure, TopologicalSpace.Closeds.mem_closure, image_closure_subset_closure_image, ContinuousLinearMap.isCompact_closure_image_coe_of_bounded, EMetric.mem_closure_iff, eventually_closure_subset_of_isOpen_of_omegaLimit_subset, Submodule.coe_closure, closure_interior_idem, Filter.le_lift'_closure, tendsto_indicator_cthickening_indicator_closure, gauge_le_one_iff_mem_closure, UniqueDiffWithinAt.closure, closure_Ico, closure_sUnion_irreducibleComponents_diff_singleton, derivedSet_closure, Submonoid.coe_topologicalClosure, Dynamics.coverEntropyInfEntourage_closure, UniformSpace.mem_closure_iff_symm_ball, closure_discrete, vadd_closure_orbit_subset, Topology.IsUpperSet.closure_singleton, Dynamics.coverEntropyEntourage_closure, mem_closure_iff_nhds_ne_bot, IsIrreducible.closure_genericPoint, subset_closure_inter_union_closure_compl_right, compl_add_closure_zero_eq_iff, TopologicalSpace.IrreducibleCloseds.coe_map, Metric.closure_eq_iInter_cthickening', Bornology.IsVonNBounded.closure, isPreirreducible_iff_forall_mem_subset_closure_singleton, Metric.infDist_pos_iff_notMem_closure, TotallyBounded.closure, IsOpenMap.preimage_closure_subset_closure_preimage, inseparable_iff_closure_eq, upperBounds_closure, closure_eq_inter_uniformity, bddAbove_closure, mem_closure_of_gauge_le_one, interior_eq_compl_closure_compl, clusterPt_iff_lift'_closure, disjoint_lift'_closure_nhds, isClosed_preimage_val, UniqueDiffWithinAt.mem_closure, IsCompact.lift'_closure_nhdsSet, closedAbsConvexHull_eq_closure_absConvexHull, AlgebraicGeometry.Scheme.Hom.support_ker, IsOpen.frontier_eq, Filter.Frequently.mem_closure, closure_eq_compl_interior_compl, AddSubsemigroup.top_closure_add_self_subset, TopologicalSpace.Closeds.coe_closure, IsPreirreducible.closure, IsCompactOperator.isCompact_closure_image_of_bounded, specializingMap_iff_isClosed_image_closure_singleton, Set.Subsingleton.closure, interior_compl, closure_ball, frontier_subset_closure, Metric.cthickening_of_nonpos, ClusterPt.mem_closure_of_mem, EMetric.hausdorffEdist_closure, Topology.IsInducing.dense_iff, Metric.closedBall_infDist_compl_subset_closure, exists_isClosed_iff, specializingMap_iff_closure_singleton, isCompact_closure_of_isTightMeasureSet, Disjoint.closure_left, IsOpen.closure_mul, closure_ae_eq_of_null_frontier, seqClosure_subset_closure, asymptoticCone_submodule, closure_empty, specializingMap_iff_stableUnderSpecialization_image_singleton, closure_induced, t0Space_iff_or_notMem_closure, NumberField.mixedEmbedding.fundamentalCone.compactSet_ae, FrechetUrysohnSpace.closure_subset_seqClosure, ClosedSubmodule.coe_iSup, IsOpen.mul_closure, closure_subset_closedConvexHull, csSup_mem_closure, Metric.exists_mem_closure_infDist_eq_dist, interior_subset_closure, derivedSet_subset_closure, Submonoid.top_closure_mul_self_eq, normal_exists_closure_subset, ContinuousAlgEquiv.preimage_closure, Specializes.closure_subset, AddSubmonoid.coe_topologicalClosure, closure_compl_singleton, closure_diff_intrinsicInterior, Set.UniformEquicontinuous.closure, zero_mem_tangentConeAt_iff, Convex.closure_subset_image_homothety_interior_of_one_lt, compl_mul_closure_one_eq_iff, mulIndicator_cthickening_eventually_eq_mulIndicator_closure, Metric.isCover_closure, lowerBounds_closure, IsCompactOperator.isCompact_closure_image_ball, UniformSpace.closure_subset_preimage, IsClosed.add_closure_zero_eq, ConvexCone.closure_eq, ContinuousLinearEquiv.preimage_closure, ContinuousMap.ker_evalStarAlgHom_eq_closure_adjoin_id, closure_subset_preimage_closure_image, Complex.eqOn_closure_of_eqOn_frontier, IsClosedMap.closure_image_eq_of_continuous, segment_subset_closure_openSegment, isClosed_closure, Filter.HasBasis.tangentConeAt_eq_biInter_closure, closure_range_zpow_eq_pow, Metric.closure_subset_thickening, closure_diff_interior, disjoint_nhdsSet_nhds, mulIndicator_thickening_eventually_eq_mulIndicator_closure, MeasureTheory.Measure.haar.haarContent_outerMeasure_closure_pos, Filter.HasBasis.lift'_closure, continuous_iff_image_closure_subset_closure_image, asymptoticCone_eq_closure_of_forall_smul_mem, isCompact_closure_of_totallyBounded_quasiComplete, EMetric.hausdorffEdist_self_closure, omegaLimit_subset_closure_fw_image, inv_closure, tendsto_subseq_of_bounded, closure_iUnion₂_le_nat, Set.EquicontinuousOn.closure, isIrreducible_iff_closure, closure_halfSpace, closure_image_mem_nhds_of_isUniformInducing, IsLocallyClosed.isOpen_preimage_val_closure, LinearEquiv.image_closure_of_convex', ClosedSubmodule.coe_sup, tendsto_mulIndicator_cthickening_mulIndicator_closure, EMetric.subset_countable_closure_of_compact, PrimeSpectrum.vanishingIdeal_closure, ProjectiveSpectrum.le_iff_mem_closure, frontier_inter_subset, Complex.frontier_reProdIm, IsCompact.mem_closure_iff_exists_inseparable, closure_smul, Euclidean.closure_ball, Filter.HasBasis.clusterPt_iff_forall_mem_closure, Real.mem_closure_iff, closure_subset_closedAbsConvexHull, EMetric.hausdorffEdist_closure₂, closure_eq_interior_union_frontier, IsOpen.exists_positiveCompacts_closure_subset, exists_isOpen_superset_and_isCompact_closure, Union_closure_singleton_eq_iff, ExtremallyDisconnected.disjoint_closure_of_disjoint_isOpen, omegaLimit_eq_iInter, closure_univ, csInf_mem_closure, addGroup_inseparable_iff, Topology.IsInducing.closure_eq_preimage_closure_image, neg_closure, IsCompact.closure_of_subset, mem_closure_iff_nhds_basis, specializes_iff_closure_subset, intrinsicClosure_eq_closure, tendsto_indicator_thickening_indicator_closure, NonUnitalSubsemiring.topologicalClosure_coe, intrinsicClosure_subset_closure, closure_lowerClosure_comm_pi, Metric.IsCover.closure, Metric.hausdorffDist_closure₁, NumberField.mixedEmbedding.fundamentalCone.compactSet_eq_union, Topology.RelCWComplex.closure_openCell_eq_closedCell, closure_sUnion, Set.EquicontinuousAt.closure, PrimeSpectrum.vanishingIdeal_mem_minimalPrimes, omegaLimit_eq_iInter_inter, IsUpperSet.closure, closure_range_zsmul_eq_nsmul, HasUpperLowerClosure.isUpperSet_closure, stableUnderSpecialization_iff_Union_eq, PointedCone.closure_eq, MeasureTheory.exists_isCompact_closure_measure_compl_lt, tendsto_subseq_of_frequently_bounded, Continuous.closure_preimage_subset, mem_closure_of_nonempty_tangentConeAt, IsClosedMap.mapClusterPt_iff_lift'_closure, measure_closure_of_null_frontier, MeasureTheory.Measure.support_restrict_subset, Topology.IsEmbedding.closure_eq_preimage_closure_image, exists_isOpen_mem_isCompact_closure, PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure, specializes_TFAE, AddSubgroup.topologicalClosure_coe, closure_singleton_eq_Iic, ConvexCone.mem_closure, Filter.HasBasis.nhds_closure, MeasureTheory.innerRegularWRT_isCompact_closure, closure_inter_open_nonempty_iff, closure_vadd, EMetric.hausdorffEdist_closure₁, SeminormedCommGroup.mem_closure_iff, IsCompactOperator.isCompact_closure_image_closedBall, ContinuousLinearMap.closure_preimage, sSup_mem_closure, Metric.closure_eq_iInter_thickening, closure_diff_frontier, IsCompactOperator.isCompact_closure_image_of_isVonNBounded, Set.EquicontinuousWithinAt.closure, Dense.closure, closure_prod_eq, mem_closure_of_tendsto, monotone_closure, ite_inter_closure_eq_of_inter_frontier_eq, extChartAt_target_subset_closure_interior, mem_intrinsicClosure, Metric.thickening_closure, Topology.IsLower.closure_singleton, Topology.IsScott.closure_singleton, closedAbsConvexHull_closure_eq_closedAbsConvexHull, Metric.infEDist_pos_iff_notMem_closure, EquicontinuousWithinAt.closure', closure_Ioc, MeasureTheory.Measure.OuterRegular.measure_closure_eq_of_isCompact, NumberField.mixedEmbedding.fundamentalCone.closure_paramSet_ae_interior, closure_Ioi, closure_diff, Complex.closure_setOf_im_lt, closure_Ioo, Bornology.IsBounded.closure, MeasureTheory.measure_mul_closure_one, smul_closure_subset
coborder 📖	CompOp	19 math math: dense_coborder, coborder_inter_closure, coborder_preimage, coborder_eq_compl_frontier_iff, closure_inter_coborder, IsClosed.coborder_eq, coborder_eq_univ_iff, coborder_eq_union_frontier_compl, coborder_eq_union_closure_compl, isClosed_preimage_val_coborder, isLocallyClosed_tfae, IsOpen.coborder_eq, Continuous.preimage_coborder_subset, coborder_mem_residual, subset_coborder, IsLocallyClosed.isOpen_coborder, Topology.IsOpenEmbedding.coborder_preimage, isLocallyClosed_iff_isOpen_coborder, IsOpenMap.coborder_preimage_subset
frontier 📖	CompOp	115 math math: isClosed_frontier, frontier_compl, ContinuousLinearMap.frontier_preimage, Complex.exists_mem_frontier_isMaxOn_norm, frontier_halfSpace, Metric.frontier_closedBall_subset_sphere, frontier_union_subset, compl_frontier_eq_union_interior, Complex.frontier_setOf_re_le, frontier_subset_iff_isClosed, Complex.frontier_preimage_re, frontier_Ici, NumberField.mixedEmbedding.fundamentalCone.volume_frontier_normLeOne, frontier_Ico, disjoint_interior_frontier, frontier_Ici', Complex.frontier_setOf_im_lt, frontier_Ioo, mem_intrinsicFrontier, coborder_eq_compl_frontier_iff, mem_frontier_of_gauge_eq_one, frontier_prod_eq, intrinsicFrontier_subset_frontier, self_diff_frontier, frontier_Ioi, exists_homeomorph_image_interior_closure_frontier_eq_unitBall, frontier_interior_subset, interior_frontier, frontier_lt_subset_eq, Metric.frontier_thickening_subset, frontier_range_modelWithCornersEuclideanHalfSpace, IsClosed.frontier_subset, IsClosed.frontier_eq, gauge_eq_one_iff_mem_frontier, threeAPFree_frontier, MeasureTheory.exists_null_frontier_thickening, frontier_prod_univ_eq, OpenPartialHomeomorph.preimage_frontier, Set.OrdConnected.null_frontier, coborder_eq_union_frontier_compl, Complex.frontier_preimage_im, Metric.frontier_ball_subset_sphere, disjoint_frontier_iff_isOpen, Complex.frontier_setOf_lt_im, measurableSet_frontier, frontier_closure_subset, Subalgebra.frontier_subset_frontier, frontier_Iic', Complex.frontier_setOf_le_re, Complex.frontier_setOf_re_lt, frontier_Iio', Continuous.frontier_preimage_subset, frontier_Ici_subset, frontier_sphere', Convex.addHaar_frontier, IsOpen.inter_frontier_eq, exists_homeomorph_image_eq, IsUltrametricDist.frontier_closedBall_eq_empty, frontier_Ioc, IccRightChart_extend_top_mem_frontier, nonempty_frontier_iff, Metric.frontier_thickening_disjoint, closure_eq_self_union_frontier, frontier_closedBall, frontier_closedBall', Homeomorph.preimage_frontier, frontier_eq_inter_compl_interior, IsOpen.coborder_eq, Metric.frontier_cthickening_disjoint, frontier_le_subset_eq, frontier_empty, frontier_eq_closure_inter_closure, frontier_eq_empty_iff, frontier_univ, frontier_ball, Subalgebra.frontier_spectrum, MeasureTheory.exists_null_frontiers_thickening, IsUpperSet.null_frontier, Complex.frontier_setOf_le_re_and_le_im, SeparationQuotient.preimage_mk_frontier, frontier_Iic, frontier_Iic_subset, IsUltrametricDist.frontier_ball_eq_empty, isClopen_iff_frontier_eq_empty, frontier_Icc, IsOpenMap.preimage_frontier_subset_frontier_preimage, IsOpen.frontier_eq, frontier_Iio, frontier_subset_closure, frontier_sphere, IsCompact.exists_mem_frontier_infDist_compl_eq_dist, Complex.frontier_setOf_le_re_and_im_le, Metric.frontier_cthickening_subset, Homeomorph.image_frontier, frontier_inter_open_inter, Complex.frontier_setOf_lt_re, Complex.frontier_setOf_le_im, closure_diff_interior, Disjoint.frontier_right, IsLowerSet.null_frontier, OpenPartialHomeomorph.IsImage.frontier, Trivialization.frontier_preimage, Disjoint.frontier_left, frontier_inter_subset, Complex.frontier_reProdIm, closure_eq_interior_union_frontier, Complex.frontier_setOf_im_le, frontier_Ioi', ModelWithCorners.isBoundaryPoint_iff, frontier_univ_prod_eq, IsOpenMap.preimage_frontier_eq_frontier_preimage, IccLeftChart_extend_bot_mem_frontier, closure_diff_frontier, IsClopen.frontier_eq, exists_mem_frontier_infDist_compl_eq_dist
interior 📖	CompOp	264 math math: VitaliFamily.nonempty_interior, subset_interior_iff_isOpen, subset_interior_mul_left, interior_smul₀, TopologicalSpace.Opens.coe_interior, Filter.EventuallyEq.mem_interior_iff, Convex.nontrivial_iff_nonempty_interior, closure_interior_Icc, subset_interior_div, exists_compact_between, NumberField.mixedEmbedding.fundamentalCone.interior_paramSet, subset_interior_add', ProbabilityTheory.eqOn_complexMGF_of_mgf', OpenPartialHomeomorph.restr_target, ProbabilityTheory.analyticOn_mgf, interior_subset_intrinsicInterior, Homeomorph.image_interior, IsGδ.dense_sUnion_interior_of_closed, subset_interior_iff_nhds, compl_frontier_eq_union_interior, IsOpenMap.image_interior_subset, MeasureTheory.Measure.interior_eq_empty_of_null, subset_interior_mul', interior_Ici, ContinuousMap.setOfIdeal_ofSet_eq_interior, mem_interior_iff_mem_nhds, interior_subset, IsLowerSet.exists_subset_ball, Set.Finite.interior_sInter, Ioo_subset_closure_interior, OpenPartialHomeomorph.preimage_interior, interior_inter, interior_closedBall, interior_convexHull_nonempty_iff_affineSpan_eq_top, ConcaveOn.locallyLipschitzOn_interior, ConvexOn.monotoneOn_rightDeriv, interior_iInter₂_subset, interior_mono, interior_univ, upperClosure_interior_subset', dense_iUnion_interior_of_closed, interior_empty, IsUpperSet.interior, IsGδ.dense_biUnion_interior_of_closed, disjoint_interior_frontier, AffineBasis.interior_convexHull, Complex.interior_setOf_le_re, NumberField.mixedEmbedding.fundamentalCone.volume_interior_eq_volume_closure, subset_interior_add_left, Metric.ball_subset_interior_closedBall, Convex.combo_interior_closure_subset_interior, isOpen_interior, interior_singleton, interior_Iio, upperClosure_interior_subset, lowerClosure_interior_subset', isOpenMap_iff_image_interior, image_gaugeRescaleHomeomorph_interior, ContinuousLinearMap.interior_preimage, OpenPartialHomeomorph.restr_toPartialEquiv, self_diff_frontier, Complex.interior_preimage_re, interior_subset_iff, NumberField.mixedEmbedding.fundamentalCone.subset_interior_normLeOne, ProbabilityTheory.eqOn_complexMGF_of_mgf, IsAntichain.interior_eq_empty', isClosedMap_iff_kernImage_interior, Dense.interior_compl, Convex.combo_self_interior_subset_interior, subset_interior_add, MeasureTheory.Content.outerMeasure_interior_compacts, countable_cover_nhds_interior, frontier_interior_subset, TopologicalSpace.PositiveCompacts.interior_nonempty, interior_frontier, interior_maximal, Convex.interior_nonempty_iff_affineSpan_eq_top, dense_biUnion_interior_of_closed, exists_compact_closed_between, lift'_nhdsSet_interior, IsAntichain.interior_eq_empty, ProbabilityTheory.analyticOnNhd_cgf, extDerivWithin_extDerivWithin_eqOn, NumberField.mixedEmbedding.fundamentalCone.measurableSet_interior_paramSet, exists_mem_interior_convexHull_affineBasis, dense_sUnion_interior_of_closed, CompactExhaustion.subset_interior_succ', interior_Icc, continuous_iff_preimage_interior_subset_interior_preimage, interior_prod_eq, Complex.interior_preimage_im, ProbabilityTheory.differentiableOn_mgf, IsClosed.frontier_eq, IsOpen.subset_interior_iff, interior_union_of_disjoint_closure, IsPreirreducible.interior, subset_interior_div_right, interior_halfSpace, interior_subset_gauge_lt_one, interior_smul, preimage_interior_subset_interior_preimage, Ioc_subset_closure_interior, strictConvex_iff_openSegment_subset, StrictConvex.openSegment_subset, ProbabilityTheory.analyticOn_cgf, MeasureTheory.Measure.interior_inter_support, Complex.interior_setOf_le_im, lowerClosure_interior_subset, mem_interior_iff_not_clusterPt_compl, isNowhereDense_iff_disjoint, Convex.combo_interior_self_subset_interior, interior_iInter_subset, IsOpenMap.preimage_interior_eq_interior_preimage, Rat.interior_compact_eq_empty, interior_closure_idem, subset_interior_sub, Filter.lift'_interior_le, TopologicalSpace.PositiveCompacts.interior_nonempty', interior_sInter_subset, lt_subset_interior_le, interior_vadd, Ctop.Realizer.mem_interior_iff, interior_Iic', Complex.interior_reProdIm, ModelWithCorners.nonempty_interior, Filter.HasBasis.nhdsSet_interior, Set.OrdConnected.interior, interior_iInter₂_lt_nat, Complex.interior_setOf_im_le, interior_Ioc, Metric.thickening_subset_interior_cthickening, Convex.combo_closure_interior_subset_interior, Homeomorph.preimage_interior, CompactExhaustion.subset_interior, exists_isOpen_iff, Convex.exists_subset_interior_convexHull_finset_of_isCompact, interior_setOf_eq, Set.Finite.interior_biInter, Convex.interior, StrictConvex.centerMass_mem_interior, gc_nhdsKer_interior, forall_isOpen_iff, Topology.RelCWComplex.disjoint_interior_base_closedCell, subset_interior_union, exists_compact_subset, measurableSet_interior, ConvexOn.monotoneOn_leftDeriv, Filter.HasBasis.lift'_interior_eq_self, mapsTo_gaugeRescale_interior, IsOpen.subset_interior_closure, uniformity_eq_uniformity_interior, interior_sphere, interior_eq_nhds, ContinuousOn.preimage_interior_subset_interior_preimage, IsOpenMap.interior_preimage_subset_preimage_interior, Complex.interior_setOf_re_le, ConcaveOn.continuousOn_interior, subset_interior_iff_mem_nhdsSet, interior_eq_nhds', interior_sInter, subset_interior_iff, ConvexOn.locallyLipschitzOn_interior, nonempty_interior_of_iUnion_of_closed, interior_iInter₂_le_nat, Balanced.zero_insert_interior, Filter.mem_interior, OpenPartialHomeomorph.interior_extend_target_subset_interior_range, frontier_eq_inter_compl_interior, interior_ae_eq_of_null_frontier, interior_range_modelWithCornersEuclideanHalfSpace, StrictConvex.sum_mem_interior, subset_interior_sub_left, ProbabilityTheory.differentiableOn_complexMGF, IsClosed.isNowhereDense_iff, OpenPartialHomeomorph.IsImage.interior, ModelWithCorners.range_eq_closure_interior, ModelWithCorners.range_subset_closure_interior, OpenPartialHomeomorph.restr_source, closure_compl, IsClosed.closure_interior_subset, Ico_subset_closure_interior, gauge_lt_one_eq_interior, SeparationQuotient.preimage_mk_interior, interior_eq_iff_isOpen, TopologicalSpace.Opens.mem_interior, finite_cover_nhds_interior, IsLowerSet.mem_interior_of_forall_lt, closure_interior_idem, ProbabilityTheory.analyticOnNhd_mgf, subset_interior_smul_right, ModelWithCorners.isInteriorPoint_iff, subset_interior_vadd, interior_union_inter_interior_compl_left_subset, interior_extChartAt_target_nonempty, measure_interior_of_null_frontier, interior_iInter, IsUpperSet.exists_subset_ball, interior_Ico, interior_mem_nhds, ProbabilityTheory.analyticOn_complexMGF, subset_interior_div_left, ConvexOn.continuousOn_interior, interior_union_inter_interior_compl_right_subset, IsGδ.dense_iUnion_interior_of_closed, interior_eq_compl_closure_compl, StrictConvex.add_smul_sub_mem, IsUpperSet.mem_interior_of_forall_lt, StrictConvex.add_smul_mem, mem_interior, IsOpenMap.mapsTo_interior, isOpenMap_iff_interior, interior_mem_uniformity, Filter.HasBasis.nhds_interior, closure_eq_compl_interior_compl, interior_Ioo, interior_compl, interior_interior, interior_closedBall', IsClosed.interior_union_right, IsClosed.interior_union_left, subset_interior_smul, IsDenseInducing.interior_compact_eq_empty, StrictConvex.ae_eq_const_or_average_mem_interior, CompactExhaustion.subset_interior_succ, interior_Iic, interior_Ioi, AffineBasis.centroid_mem_interior_convexHull, gauge_lt_one_iff_mem_interior, mem_nhdsSet_interior, interior_eq_univ, interior_subset_closure, interior_pi_set, IsOpen.interior_eq, Filter.HasBasis.lift'_interior, nhdsSet_interior, subset_interior_vadd_right, interior_sphere', interior_eq_empty_iff_dense_compl, mem_intrinsicInterior, closure_diff_interior, ProbabilityTheory.analyticOnNhd_complexMGF, exists_compact_superset, lift'_nhds_interior, ModelWithCorners.nonempty_interior', ProbabilityTheory.analyticOn_iteratedDeriv_mgf, closure_eq_interior_union_frontier, ProbabilityTheory.continuousOn_mgf, StrictConvex.smul_mem_of_zero_mem, interior_euclideanQuadrant, interior_Ici', StrictConvex.mem_smul_of_zero_mem, interior_iInter_of_finite, subset_interior_add_right, subset_interior_mul_right, subset_interior_sub_right, closure_diff_frontier, extChartAt_target_subset_closure_interior, IsLowerSet.interior, Topology.RelCWComplex.disjoint_interior_base_iUnion_closedCell, NumberField.mixedEmbedding.fundamentalCone.closure_paramSet_ae_interior, subset_interior_mul, ProbabilityTheory.analyticOnNhd_iteratedDeriv_mgf, Finset.interior_iInter, MeasureTheory.Content.contentRegular_exists_compact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOpenQuotientMap_iff 📖	mathematical	—	IsOpenQuotientMap Continuous IsOpenMap	—	—
isOpen_sUnion 📖	mathematical	IsOpen	Set.sUnion	—	TopologicalSpace.isOpen_sUnion
isOpen_univ 📖	mathematical	—	IsOpen Set.univ	—	TopologicalSpace.isOpen_univ

---

← Back to Index