LocalSourceTargetProperty

📁 Source: Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean

Statistics

Metric	Count
Definitions IsLocalSourceTargetProperty, LiftSourceTargetPropertyAt, codChart, domChart, localPresentationAt, LocalPresentationAt, codChart, domChart	8
Theorems liftSourceTargetPropertyAt, mono_source, codChart_mem_maximalAtlas, congr_iff, congr_iff_of_eventuallyEq, congr_of_eventuallyEq, domChart_mem_maximalAtlas, mem_codChart_source, mem_domChart_source, mk_of_continuousAt, prodMap, property, source_subset_preimage_source, codChart_mem_maximalAtlas, domChart_mem_maximalAtlas, mem_codChart_source, mem_domChart_source, property, source_subset_preimage_source	19
Total	27

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
liftSourceTargetPropertyAt 📖	mathematical	—	IsOpen setOf Manifold.LiftSourceTargetPropertyAt	—	isOpen_iff_forall_mem_open Manifold.LiftSourceTargetPropertyAt.source_subset_preimage_source Manifold.LiftSourceTargetPropertyAt.domChart_mem_maximalAtlas Manifold.LiftSourceTargetPropertyAt.codChart_mem_maximalAtlas Manifold.LiftSourceTargetPropertyAt.property OpenPartialHomeomorph.open_source Manifold.LiftSourceTargetPropertyAt.mem_domChart_source

Manifold

Definitions

Name	Category	Theorems
IsLocalSourceTargetProperty 📖	CompData	1 math math: isLocalSourceTargetProperty_immersionAtProp
LiftSourceTargetPropertyAt 📖	MathDef	8 math math: IsImmersionAtOfComplement_def, IsOpen.liftSourceTargetPropertyAt, LiftSourceTargetPropertyAt.congr_iff_of_eventuallyEq, IsImmersionAt.property, LiftSourceTargetPropertyAt.congr_of_eventuallyEq, IsImmersionAtOfComplement.property, LiftSourceTargetPropertyAt.mk_of_continuousAt, LiftSourceTargetPropertyAt.prodMap
LocalPresentationAt 📖	CompData	—

Manifold.IsLocalSourceTargetProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mono_source 📖	mathematical	Manifold.IsLocalSourceTargetProperty IsOpen	OpenPartialHomeomorph.restr	—	—

Manifold.LiftSourceTargetPropertyAt

Definitions

Name	Category	Theorems
codChart 📖	CompOp	4 math math: property, mem_codChart_source, codChart_mem_maximalAtlas, source_subset_preimage_source
domChart 📖	CompOp	4 math math: mem_domChart_source, property, domChart_mem_maximalAtlas, source_subset_preimage_source
localPresentationAt 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
codChart_mem_maximalAtlas 📖	mathematical	—	OpenPartialHomeomorph Set Set.instMembership IsManifold.maximalAtlas codChart	—	Manifold.LocalPresentationAt.codChart_mem_maximalAtlas
congr_iff 📖	—	Manifold.IsLocalSourceTargetProperty Set.EqOn PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	—	—	Manifold.IsLocalSourceTargetProperty.congr Set.EqOn.symm
congr_iff_of_eventuallyEq 📖	mathematical	Manifold.IsLocalSourceTargetProperty Filter.EventuallyEq nhds	Manifold.LiftSourceTargetPropertyAt	—	congr_of_eventuallyEq Filter.EventuallyEq.symm
congr_of_eventuallyEq 📖	mathematical	Manifold.IsLocalSourceTargetProperty Filter.EventuallyEq nhds	Manifold.LiftSourceTargetPropertyAt	—	Filter.EventuallyEq.exists_mem mem_nhds_iff mem_domChart_source interior_eq_iff_isOpen mem_codChart_source mem_of_mem_nhds restr_mem_maximalAtlas instClosedUnderRestrictionContDiffGroupoid domChart_mem_maximalAtlas codChart_mem_maximalAtlas Set.subset_inter Set.Subset.trans source_subset_preimage_source Set.EqOn.inter_preimage_eq Set.inter_subset_right Manifold.IsLocalSourceTargetProperty.congr Set.EqOn.mono Manifold.IsLocalSourceTargetProperty.mono_source property
domChart_mem_maximalAtlas 📖	mathematical	—	OpenPartialHomeomorph Set Set.instMembership IsManifold.maximalAtlas domChart	—	Manifold.LocalPresentationAt.domChart_mem_maximalAtlas
mem_codChart_source 📖	mathematical	—	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv codChart	—	Manifold.LocalPresentationAt.mem_codChart_source
mem_domChart_source 📖	mathematical	—	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv domChart	—	Manifold.LocalPresentationAt.mem_domChart_source
mk_of_continuousAt 📖	mathematical	ContinuousAt Manifold.IsLocalSourceTargetProperty Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv OpenPartialHomeomorph IsManifold.maximalAtlas	Manifold.LiftSourceTargetPropertyAt	—	mem_nhds_iff ContinuousAt.preimage_mem_nhds IsOpen.mem_nhds OpenPartialHomeomorph.open_source restr_mem_maximalAtlas instClosedUnderRestrictionContDiffGroupoid Manifold.IsLocalSourceTargetProperty.mono_source
prodMap 📖	mathematical	OpenPartialHomeomorph.prod	Manifold.LiftSourceTargetPropertyAt ModelProd Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup instTopologicalSpaceModelProd ModelWithCorners.prod instTopologicalSpaceProd prodChartedSpace	—	mem_domChart_source mem_codChart_source IsManifold.mem_maximalAtlas_prod domChart_mem_maximalAtlas codChart_mem_maximalAtlas Set.prod_mono source_subset_preimage_source property
property 📖	mathematical	—	domChart codChart	—	Manifold.LocalPresentationAt.property
source_subset_preimage_source 📖	mathematical	—	Set Set.instHasSubset PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv domChart Set.preimage codChart	—	Manifold.LocalPresentationAt.source_subset_preimage_source

Manifold.LocalPresentationAt

Definitions

Name	Category	Theorems
codChart 📖	CompOp	4 math math: mem_codChart_source, source_subset_preimage_source, property, codChart_mem_maximalAtlas
domChart 📖	CompOp	4 math math: mem_domChart_source, source_subset_preimage_source, domChart_mem_maximalAtlas, property

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
codChart_mem_maximalAtlas 📖	mathematical	—	OpenPartialHomeomorph Set Set.instMembership IsManifold.maximalAtlas codChart	—	—
domChart_mem_maximalAtlas 📖	mathematical	—	OpenPartialHomeomorph Set Set.instMembership IsManifold.maximalAtlas domChart	—	—
mem_codChart_source 📖	mathematical	—	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv codChart	—	—
mem_domChart_source 📖	mathematical	—	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv domChart	—	—
property 📖	mathematical	—	domChart codChart	—	—
source_subset_preimage_source 📖	mathematical	—	Set Set.instHasSubset PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv domChart Set.preimage codChart	—	—

---

← Back to Index