AbstractCompletion

📁 Source: Mathlib/Topology/UniformSpace/AbstractCompletion.lean

Statistics

Metric	Count
Definitions `AbstractCompletion`, `compare`, `compareEquiv`, `extend`, `extend₂`, `map`, `mapEquiv`, `map₂`, `ofComplete`, `prod`, `space`, `uniformStruct`	12
Theorems `closure_range`, `compare_coe`, `compare_comp_eq_compare`, `complete`, `continuous_coe`, `continuous_extend`, `continuous_map`, `continuous_map₂`, `dense`, `extend_coe`, `extend_comp_coe`, `extend_def`, `extend_map`, `extend_unique`, `extension₂_coe_coe`, `funext`, `induction_on`, `inseparable_extend_coe`, `inverse_compare`, `isDenseInducing`, `isUniformInducing`, `isUniformInducing_extend`, `mapEquiv_coe`, `mapEquiv_symm`, `map_coe`, `map_comp`, `map_id`, `map_unique`, `map₂_coe_coe`, `separation`, `uniformContinuous_coe`, `uniformContinuous_compare`, `uniformContinuous_compareEquiv`, `uniformContinuous_compareEquiv_symm`, `uniformContinuous_extend`, `uniformContinuous_extension₂`, `uniformContinuous_map`, `uniformContinuous_map₂`	38
Total	50

AbstractCompletion

Definitions

Name	Category	Theorems
`compare` 📖	CompOp	7 math math: `LaurentSeries.LaurentSeriesRingEquiv_def`, `compare_coe`, `uniformContinuous_compare`, `compare_comp_eq_compare`, `inverse_compare`, `LaurentSeries.valuation_compare`, `LaurentSeries.ratfuncAdicComplRingEquiv_apply`
`compareEquiv` 📖	CompOp	2 math math: `uniformContinuous_compareEquiv`, `uniformContinuous_compareEquiv_symm`
`extend` 📖	CompOp	9 math math: `extend_map`, `extend_def`, `extend_coe`, `extend_comp_coe`, `inseparable_extend_coe`, `uniformContinuous_extend`, `extend_unique`, `isUniformInducing_extend`, `continuous_extend`
`extend₂` 📖	CompOp	2 math math: `extension₂_coe_coe`, `uniformContinuous_extension₂`
`map` 📖	CompOp	7 math math: `extend_map`, `map_coe`, `uniformContinuous_map`, `continuous_map`, `map_unique`, `map_comp`, `map_id`
`mapEquiv` 📖	CompOp	2 math math: `mapEquiv_coe`, `mapEquiv_symm`
`map₂` 📖	CompOp	3 math math: `uniformContinuous_map₂`, `continuous_map₂`, `map₂_coe_coe`
`ofComplete` 📖	CompOp	—
`prod` 📖	CompOp	—
`space` 📖	CompOp	26 math math: `uniformContinuous_map₂`, `mapEquiv_coe`, `dense`, `uniformContinuous_compare`, `extend_map`, `continuous_coe`, `closure_range`, `uniformContinuous_compareEquiv`, `uniformContinuous_coe`, `extend_def`, `separation`, `inverse_compare`, `LaurentSeries.valuation_LaurentSeries_equal_extension`, `mapEquiv_symm`, `uniformContinuous_extend`, `uniformContinuous_map`, `continuous_map`, `isUniformInducing`, `uniformContinuous_extension₂`, `complete`, `map_comp`, `isDenseInducing`, `isUniformInducing_extend`, `continuous_extend`, `uniformContinuous_compareEquiv_symm`, `map_id`
`uniformStruct` 📖	CompOp	22 math math: `uniformContinuous_map₂`, `mapEquiv_coe`, `dense`, `uniformContinuous_compare`, `continuous_coe`, `closure_range`, `uniformContinuous_compareEquiv`, `uniformContinuous_coe`, `extend_def`, `separation`, `LaurentSeries.valuation_LaurentSeries_equal_extension`, `mapEquiv_symm`, `uniformContinuous_extend`, `uniformContinuous_map`, `continuous_map`, `isUniformInducing`, `uniformContinuous_extension₂`, `complete`, `isDenseInducing`, `isUniformInducing_extend`, `continuous_extend`, `uniformContinuous_compareEquiv_symm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_range` 📖	mathematical	—	`closure` `space` `UniformSpace.toTopologicalSpace` `uniformStruct` `Set.range` `coe` `Set.univ`	—	`DenseRange.closure_range` `dense`
`compare_coe` 📖	mathematical	—	`compare` `coe`	—	`extend_coe` `T25Space.t2Space` `T3Space.t25Space` `instT3Space` `separation` `UniformSpace.to_regularSpace` `uniformContinuous_coe`
`compare_comp_eq_compare` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `Filter.Tendsto` `Filter.comap` `space` `coe` `nhds` `uniformStruct` `IsDenseInducing.extend` `isDenseInducing`	`compare`	—	`isDenseInducing` `IsDenseInducing.extend.congr_simp` `compare_coe` `IsDenseInducing.extend_eq` `T25Space.t2Space` `T3Space.t25Space` `IsDenseInducing.extend_unique` `Continuous.comp` `IsDenseInducing.continuous_extend` `UniformContinuous.continuous` `uniformContinuous_compare`
`complete` 📖	mathematical	—	`CompleteSpace` `space` `uniformStruct`	—	—
`continuous_coe` 📖	mathematical	—	`Continuous` `space` `UniformSpace.toTopologicalSpace` `uniformStruct` `coe`	—	`UniformContinuous.continuous` `uniformContinuous_coe`
`continuous_extend` 📖	mathematical	—	`Continuous` `space` `UniformSpace.toTopologicalSpace` `uniformStruct` `extend`	—	`UniformContinuous.continuous` `uniformContinuous_extend`
`continuous_map` 📖	mathematical	—	`Continuous` `space` `UniformSpace.toTopologicalSpace` `uniformStruct` `map`	—	`continuous_extend` `complete`
`continuous_map₂` 📖	mathematical	`Continuous` `space` `UniformSpace.toTopologicalSpace` `uniformStruct`	`map₂`	—	`Continuous.comp₂` `UniformContinuous.continuous` `uniformContinuous_map₂`
`dense` 📖	mathematical	—	`DenseRange` `space` `UniformSpace.toTopologicalSpace` `uniformStruct` `coe`	—	—
`extend_coe` 📖	mathematical	`UniformContinuous`	`extend` `coe`	—	`isDenseInducing` `extend_def` `IsDenseInducing.extend_eq` `UniformContinuous.continuous`
`extend_comp_coe` 📖	mathematical	`UniformContinuous` `space` `uniformStruct`	`extend` `coe`	—	`induction_on` `isClosed_eq` `T25Space.t2Space` `T3Space.t25Space` `instT3Space` `UniformSpace.to_regularSpace` `continuous_extend` `UniformContinuous.continuous` `extend_coe` `UniformContinuous.comp` `uniformContinuous_coe`
`extend_def` 📖	mathematical	`UniformContinuous`	`extend` `IsDenseInducing.extend` `space` `UniformSpace.toTopologicalSpace` `uniformStruct` `coe` `isDenseInducing`	—	`isDenseInducing` `dense`
`extend_map` 📖	mathematical	`UniformContinuous`	`space` `extend` `map`	—	`funext` `T25Space.t2Space` `T3Space.t25Space` `instT3Space` `UniformSpace.to_regularSpace` `Continuous.comp` `continuous_extend` `continuous_map` `extend_coe` `UniformContinuous.comp` `map_coe`
`extend_unique` 📖	mathematical	`UniformContinuous` `space` `uniformStruct` `coe`	`extend`	—	`funext` `T25Space.t2Space` `T3Space.t25Space` `instT3Space` `UniformSpace.to_regularSpace` `continuous_extend` `UniformContinuous.continuous` `extend_coe`
`extension₂_coe_coe` 📖	mathematical	`UniformContinuous` `instUniformSpaceProd`	`extend₂` `coe`	—	`extend_coe` `T25Space.t2Space` `T3Space.t25Space` `instT3Space` `UniformSpace.to_regularSpace`
`funext` 📖	—	`Continuous` `space` `UniformSpace.toTopologicalSpace` `uniformStruct` `coe`	—	—	`induction_on` `isClosed_eq`
`induction_on` 📖	—	`coe`	—	—	`isClosed_property` `dense`
`inseparable_extend_coe` 📖	mathematical	`UniformContinuous`	`Inseparable` `UniformSpace.toTopologicalSpace` `extend` `coe`	—	`isDenseInducing` `extend_def` `IsDenseInducing.inseparable_extend` `instR1Space` `UniformSpace.to_regularSpace` `Continuous.continuousAt` `UniformContinuous.continuous`
`inverse_compare` 📖	mathematical	—	`space` `compare`	—	`uniformContinuous_compare` `funext` `T25Space.t2Space` `T3Space.t25Space` `instT3Space` `separation` `UniformSpace.to_regularSpace` `UniformContinuous.continuous` `UniformContinuous.comp` `continuous_id` `compare_coe`
`isDenseInducing` 📖	mathematical	—	`IsDenseInducing` `space` `UniformSpace.toTopologicalSpace` `uniformStruct` `coe`	—	`IsUniformInducing.isInducing` `isUniformInducing` `dense`
`isUniformInducing` 📖	mathematical	—	`IsUniformInducing` `space` `uniformStruct` `coe`	—	—
`isUniformInducing_extend` 📖	mathematical	`IsUniformInducing`	`space` `uniformStruct` `extend`	—	`isDenseInducing` `extend_def` `IsUniformInducing.uniformContinuous` `IsDenseInducing.isUniformInducing_extend` `complete` `isUniformInducing`
`mapEquiv_coe` 📖	mathematical	—	`DFunLike.coe` `UniformEquiv` `space` `uniformStruct` `EquivLike.toFunLike` `UniformEquiv.instEquivLike` `mapEquiv` `coe`	—	`map_coe` `UniformEquiv.uniformContinuous`
`mapEquiv_symm` 📖	mathematical	—	`UniformEquiv.symm` `space` `uniformStruct` `mapEquiv`	—	—
`map_coe` 📖	mathematical	`UniformContinuous`	`map` `coe`	—	`extend_coe` `T25Space.t2Space` `T3Space.t25Space` `instT3Space` `separation` `UniformSpace.to_regularSpace` `UniformContinuous.comp` `uniformContinuous_coe`
`map_comp` 📖	mathematical	`UniformContinuous`	`space` `map`	—	`extend_map` `complete` `separation` `UniformContinuous.comp` `uniformContinuous_coe`
`map_id` 📖	mathematical	—	`map` `space`	—	`map_unique` `uniformContinuous_id`
`map_unique` 📖	mathematical	`UniformContinuous` `space` `uniformStruct` `coe`	`map`	—	`funext` `T25Space.t2Space` `T3Space.t25Space` `instT3Space` `separation` `UniformSpace.to_regularSpace` `continuous_map` `UniformContinuous.continuous` `extend_coe` `UniformContinuous.comp` `uniformContinuous_coe`
`map₂_coe_coe` 📖	mathematical	`UniformContinuous₂`	`map₂` `coe`	—	`extension₂_coe_coe` `separation` `UniformContinuous.comp` `uniformContinuous_coe`
`separation` 📖	mathematical	—	`T0Space` `space` `UniformSpace.toTopologicalSpace` `uniformStruct`	—	—
`uniformContinuous_coe` 📖	mathematical	—	`UniformContinuous` `space` `uniformStruct` `coe`	—	`IsUniformInducing.uniformContinuous` `isUniformInducing`
`uniformContinuous_compare` 📖	mathematical	—	`UniformContinuous` `space` `uniformStruct` `compare`	—	`uniformContinuous_extend` `complete`
`uniformContinuous_compareEquiv` 📖	mathematical	—	`UniformContinuous` `space` `uniformStruct` `DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `UniformEquiv.instEquivLike` `compareEquiv`	—	`uniformContinuous_compare`
`uniformContinuous_compareEquiv_symm` 📖	mathematical	—	`UniformContinuous` `space` `uniformStruct` `DFunLike.coe` `UniformEquiv` `EquivLike.toFunLike` `UniformEquiv.instEquivLike` `UniformEquiv.symm` `compareEquiv`	—	`uniformContinuous_compare`
`uniformContinuous_extend` 📖	mathematical	—	`UniformContinuous` `space` `uniformStruct` `extend`	—	`isDenseInducing` `extend_def` `uniformContinuous_uniformly_extend` `isUniformInducing` `dense` `uniformContinuous_of_const`
`uniformContinuous_extension₂` 📖	mathematical	—	`UniformContinuous₂` `space` `uniformStruct` `extend₂`	—	`uniformContinuous₂_def` `extend₂.eq_1` `uniformContinuous_extend`
`uniformContinuous_map` 📖	mathematical	—	`UniformContinuous` `space` `uniformStruct` `map`	—	`uniformContinuous_extend` `complete`
`uniformContinuous_map₂` 📖	mathematical	—	`UniformContinuous₂` `space` `uniformStruct` `map₂`	—	`uniformContinuous_extension₂` `complete`

(root)

Definitions

Name	Category	Theorems
`AbstractCompletion` 📖	CompData	—

---

← Back to Index