DenseEmbedding

📁 Source: Mathlib/Topology/DenseEmbedding.lean

Statistics

Metric	Count
Definitions extend, IsDenseEmbedding, subtypeEmb, IsDenseInducing, extend	5
Theorems comap_val_nhds_neBot, continuousAt_extend, continuous_extend, extend_eq, extend_eq_at, extend_eq_of_tendsto, extend_unique, extend_unique_at, isDenseEmbedding_val, isDenseInducing_val, equalizer, induction_on, induction_on₂, induction_on₃, hasBasis_of_isDenseInducing, dense_image, id, inj_iff, injective, isDenseInducing, isEmbedding, mk', prodMap, separableSpace, subtype, subtypeEmb_coe, toIsDenseInducing, closure_image_mem_nhds, closure_range, comap_nhds_neBot, continuous, continuousAt_extend, continuous_extend, dense, dense_image, extend_eq, extend_eq', extend_eq_at, extend_eq_at', extend_eq_of_tendsto, extend_unique, extend_unique_at, inseparable_extend, interior_compact_eq_empty, isInducing, mk', nhdsWithin_neBot, nhds_eq_comap, preconnectedSpace, prodMap, separableSpace, tendsto_comap_nhds_nhds, tendsto_extend, toIsInducing, isClosed_property, isClosed_property2, isClosed_property3	57
Total	62

Dense

Definitions

Name	Category	Theorems
extend 📖	CompOp	11 math math: extend_eq_at, extend_unique_at, lipschitzWith_extend, uniformContinuous_extend, continuous_extend, extend_unique, extend_eq, extend_of_ind, extend_spec, continuousAt_extend, extend_eq_of_tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_val_nhds_neBot 📖	mathematical	Dense	Filter.NeBot Set Set.instMembership Filter.comap nhds	—	IsDenseInducing.comap_nhds_neBot isDenseInducing_val
continuousAt_extend 📖	mathematical	Dense Filter.Eventually Filter.Tendsto Set.Elem Filter.comap Set Set.instMembership nhds	ContinuousAt extend	—	IsDenseInducing.continuousAt_extend isDenseInducing_val
continuous_extend 📖	mathematical	Dense Filter.Tendsto Set.Elem Filter.comap Set Set.instMembership nhds	Continuous extend	—	IsDenseInducing.continuous_extend isDenseInducing_val
extend_eq 📖	mathematical	Dense Continuous Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	extend	—	extend_eq_at Continuous.continuousAt
extend_eq_at 📖	mathematical	Dense ContinuousAt Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	extend	—	IsDenseInducing.extend_eq_at isDenseInducing_val
extend_eq_of_tendsto 📖	mathematical	Dense Filter.Tendsto Set.Elem Filter.comap Set Set.instMembership nhds	extend	—	IsDenseInducing.extend_eq_of_tendsto isDenseInducing_val
extend_unique 📖	mathematical	Dense Set Set.instMembership Continuous	extend	—	IsDenseInducing.extend_unique isDenseInducing_val
extend_unique_at 📖	mathematical	Dense Filter.Eventually Set.Elem Set Set.instMembership Filter.comap nhds ContinuousAt	extend	—	IsDenseInducing.extend_unique_at isDenseInducing_val
isDenseEmbedding_val 📖	mathematical	Dense	IsDenseEmbedding Set Set.instMembership instTopologicalSpaceSubtype	—	Topology.IsEmbedding.subtypeVal Topology.IsEmbedding.toIsInducing denseRange_val Topology.IsEmbedding.injective
isDenseInducing_val 📖	mathematical	Dense	IsDenseInducing instTopologicalSpaceSubtype	—	Topology.IsInducing.subtypeVal denseRange_val

DenseRange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equalizer 📖	—	DenseRange Continuous	—	—	induction_on isClosed_eq
induction_on 📖	—	DenseRange	—	—	isClosed_property
induction_on₂ 📖	—	DenseRange	—	—	isClosed_property2
induction_on₃ 📖	—	DenseRange	—	—	isClosed_property3

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasBasis_of_isDenseInducing 📖	mathematical	Filter.HasBasis nhds IsDenseInducing	closure Set.image	—	Filter.hasBasis_iff exists_mem_nhds_isClosed_subset Topology.IsInducing.nhds_eq_comap IsDenseInducing.isInducing Set.Subset.rfl HasSubset.Subset.trans Set.instIsTransSubset closure_mono Set.image_mono Set.Subset.trans closure_minimal Set.image_preimage_subset IsDenseInducing.closure_image_mem_nhds Filter.mp_mem Filter.univ_mem'

IsDenseEmbedding

Definitions

Name	Category	Theorems
subtypeEmb 📖	CompOp	3 math math: subtypeEmb_coe, isUniformEmbedding_subtypeEmb, subtype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dense_image 📖	mathematical	IsDenseEmbedding	Dense Set.image	—	IsDenseInducing.dense_image isDenseInducing
id 📖	mathematical	—	IsDenseEmbedding	—	Topology.IsEmbedding.id Topology.IsEmbedding.toIsInducing denseRange_id Topology.IsEmbedding.injective
inj_iff 📖	—	IsDenseEmbedding	—	—	injective
injective 📖	—	IsDenseEmbedding	—	—	—
isDenseInducing 📖	mathematical	IsDenseEmbedding	IsDenseInducing	—	toIsDenseInducing
isEmbedding 📖	mathematical	IsDenseEmbedding	Topology.IsEmbedding	—	IsDenseInducing.toIsInducing toIsDenseInducing injective
mk' 📖	mathematical	Continuous DenseRange Set Filter Filter.instMembership nhds Set.instMembership	IsDenseEmbedding	—	IsDenseInducing.mk'
prodMap 📖	mathematical	IsDenseEmbedding	instTopologicalSpaceProd	—	IsDenseInducing.prodMap isDenseInducing Function.Injective.prodMap injective
separableSpace 📖	mathematical	IsDenseEmbedding	TopologicalSpace.SeparableSpace	—	IsDenseInducing.separableSpace isDenseInducing
subtype 📖	mathematical	IsDenseEmbedding	Set Set.instMembership closure Set.image setOf instTopologicalSpaceSubtype subtypeEmb	—	induced_iff_nhds_eq nhds_subtype_eq_comap Topology.IsInducing.nhds_eq_comap IsDenseInducing.isInducing toIsDenseInducing Filter.comap_comap dense_iff_closure_eq Set.ext Set.image_eq_range Function.Injective.codRestrict injective Subtype.coe_injective
subtypeEmb_coe 📖	mathematical	—	Set Set.instMembership closure Set.image setOf subtypeEmb	—	—
toIsDenseInducing 📖	mathematical	IsDenseEmbedding	IsDenseInducing	—	—

IsDenseInducing

Definitions

Name	Category	Theorems
extend 📖	CompOp	22 math math: uniformly_extend_unique, MvPowerSeries.eval₂Hom_eq_extend, extend_Z_bilin, continuousAt_extend, uniformContinuous_uniformly_extend, extend_unique, isUniformInducing_extend, AbstractCompletion.extend_def, uniformly_extend_of_ind, extend_eq_of_tendsto, LaurentSeries.valuation_LaurentSeries_equal_extension, continuous_extend, continuous_extend_of_cauchy, extend_eq', extend_unique_at, Padic.coe_withValRingEquiv_symm, extend_eq_at, uniformly_extend_spec, extend_eq_at', inseparable_extend, extend_eq, tendsto_extend

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_image_mem_nhds 📖	mathematical	IsDenseInducing Set Filter Filter.instMembership nhds	closure Set.image	—	Filter.HasBasis.mem_iff Filter.HasBasis.comap nhds_basis_opens nhds_eq_comap Filter.mem_of_superset IsOpen.mem_nhds DenseRange.subset_closure_image_preimage_of_isOpen dense closure_mono Set.image_mono
closure_range 📖	mathematical	IsDenseInducing	closure Set.range Set.univ	—	DenseRange.closure_range dense
comap_nhds_neBot 📖	mathematical	IsDenseInducing	Filter.NeBot Filter.comap nhds	—	Filter.comap_neBot mem_closure_iff_nhds dense
continuous 📖	mathematical	IsDenseInducing	Continuous	—	Topology.IsInducing.continuous isInducing
continuousAt_extend 📖	mathematical	IsDenseInducing Filter.Eventually Filter.Tendsto Filter.comap nhds	ContinuousAt extend	—	Filter.mp_mem Filter.univ_mem' extend_eq_of_tendsto T25Space.t2Space T3Space.t25Space Filter.HasBasis.tendsto_left_iff Filter.HasBasis.comap nhds_basis_opens' mem_of_mem_nhds IsOpen.mem_nhds IsClosed.mem_of_tendsto comap_nhds_neBot Filter.inter_mem Filter.HasBasis.tendsto_right_iff closed_nhds_basis T3Space.toRegularSpace
continuous_extend 📖	mathematical	IsDenseInducing Filter.Tendsto Filter.comap nhds	Continuous extend	—	continuous_iff_continuousAt continuousAt_extend Filter.univ_mem'
dense 📖	mathematical	IsDenseInducing	DenseRange	—	—
dense_image 📖	mathematical	IsDenseInducing	Dense Set.image	—	Topology.IsInducing.closure_eq_preimage_closure_image isInducing Dense.closure_eq Set.preimage_univ DenseRange.dense_image dense continuous
extend_eq 📖	mathematical	IsDenseInducing Continuous	extend	—	extend_eq_at Continuous.continuousAt
extend_eq' 📖	mathematical	IsDenseInducing Filter.Tendsto Filter.comap nhds	extend	—	extend_eq_at' Topology.IsInducing.nhds_eq_comap isInducing
extend_eq_at 📖	mathematical	IsDenseInducing ContinuousAt	extend	—	extend_eq_of_tendsto nhds_eq_comap
extend_eq_at' 📖	mathematical	IsDenseInducing Filter.Tendsto nhds	extend	—	extend_eq_at continuousAt_of_tendsto_nhds T2Space.t1Space
extend_eq_of_tendsto 📖	mathematical	IsDenseInducing Filter.Tendsto Filter.comap nhds	extend	—	Filter.Tendsto.limUnder_eq comap_nhds_neBot
extend_unique 📖	mathematical	IsDenseInducing Continuous	extend	—	extend_unique_at Filter.Eventually.of_forall Continuous.continuousAt
extend_unique_at 📖	mathematical	IsDenseInducing Filter.Eventually Filter.comap nhds ContinuousAt	extend	—	extend_eq_of_tendsto Filter.mem_map Filter.eventually_comap Filter.Eventually.mono Filter.Tendsto.eventually Filter.Eventually.mp
inseparable_extend 📖	mathematical	IsDenseInducing ContinuousAt	Inseparable extend	—	tendsto_nhds_unique_inseparable nhds_neBot tendsto_extend
interior_compact_eq_empty 📖	mathematical	IsDenseInducing Dense Compl.compl Set Set.instCompl Set.range IsCompact	interior Set.instEmptyCollection	—	Set.eq_empty_iff_forall_notMem closure_image_mem_nhds mem_interior_iff_mem_nhds Dense.inter_nhds_nonempty IsClosed.closure_eq IsCompact.isClosed IsCompact.image continuous Set.image_subset_range
isInducing 📖	mathematical	IsDenseInducing	Topology.IsInducing	—	toIsInducing
mk' 📖	mathematical	Continuous Set Set.instMembership closure Set.range Filter Filter.instMembership nhds	IsDenseInducing	—	Topology.isInducing_iff_nhds le_antisymm Filter.Tendsto.le_comap Continuous.tendsto
nhdsWithin_neBot 📖	mathematical	IsDenseInducing	Filter.NeBot nhdsWithin Set.range	—	DenseRange.nhdsWithin_neBot dense
nhds_eq_comap 📖	mathematical	IsDenseInducing	nhds Filter.comap	—	Topology.IsInducing.nhds_eq_comap isInducing
preconnectedSpace 📖	mathematical	IsDenseInducing	PreconnectedSpace	—	DenseRange.preconnectedSpace dense continuous
prodMap 📖	mathematical	IsDenseInducing	instTopologicalSpaceProd	—	Topology.IsInducing.prodMap isInducing DenseRange.prodMap dense
separableSpace 📖	mathematical	IsDenseInducing	TopologicalSpace.SeparableSpace	—	DenseRange.separableSpace dense continuous
tendsto_comap_nhds_nhds 📖	mathematical	IsDenseInducing Filter.Tendsto nhds	Filter.comap	—	Filter.map_comap_le Filter.map_mono Filter.comap_mono le_trans Filter.map_le_iff_le_comap Filter.map_map nhds_eq_comap
tendsto_extend 📖	mathematical	IsDenseInducing ContinuousAt	Filter.Tendsto nhds extend	—	extend.eq_1 nhds_eq_comap tendsto_nhds_limUnder
toIsInducing 📖	mathematical	IsDenseInducing	Topology.IsInducing	—	—

(root)

Definitions

Name	Category	Theorems
IsDenseEmbedding 📖	CompData	13 math math: isDenseEmbedding_stoneCechUnit, MeasureTheory.Lp.simpleFunc.isDenseEmbedding, Rat.isDenseEmbedding_coe_real, isDenseEmbedding_pure, IsDenseEmbedding.id, IsUniformEmbedding.isDenseEmbedding, IsHomeomorph.isDenseEmbedding, CauchyFilter.isDenseEmbedding_pureCauchy, Homeomorph.isDenseEmbedding, IsDenseEmbedding.mk', OnePoint.isDenseEmbedding_coe, Dense.isDenseEmbedding_val, UniformSpace.Completion.isDenseEmbedding_coe
IsDenseInducing 📖	CompData	14 math math: IsDenseEmbedding.toIsDenseInducing, IsDenseEmbedding.isDenseInducing, isDenseInducing_stoneCechUnit, IsUniformInducing.isDenseInducing, MvPolynomial.toMvPowerSeries_isDenseInducing, IsDenseInducing.mk', isDenseInducing_pure, CauchyFilter.isDenseInducing_pureCauchy, MeasureTheory.Lp.simpleFunc.isDenseInducing, UniformSpace.Completion.isDenseInducing_toCompl, AbstractCompletion.isDenseInducing, Padic.isDenseInducing_cast_withVal, Dense.isDenseInducing_val, UniformSpace.Completion.isDenseInducing_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isClosed_property 📖	—	DenseRange	—	—	DenseRange.closure_range closure_mono Set.range_subset_iff IsClosed.closure_eq
isClosed_property2 📖	—	DenseRange	—	—	isClosed_property DenseRange.prodMap
isClosed_property3 📖	—	DenseRange	—	—	isClosed_property DenseRange.prodMap

---

← Back to Index