LocalInvariantProperties

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

Statistics

Metric	Count
Definitions LiftProp, LiftPropAt, LiftPropOn, LiftPropWithinAt, IsLocalStructomorphWithinAt, LocalInvariantProp	6
Theorems continuousWithinAt, prop, liftPropAt_iff, liftPropWithinAt_iff', liftProp_iff, isLocalStructomorphWithinAt_iff, isLocalStructomorphWithinAt_iff', isLocalStructomorphWithinAt_source_iff, comp, congr', congr_iff, congr_iff_nhdsWithin, congr_nhdsWithin, congr_nhdsWithin', congr_of_forall, congr_set, is_local, is_local_nhds, left_invariance, left_invariance', liftPropAt_chart, liftPropAt_chart_symm, liftPropAt_congr_iff_of_eventuallyEq, liftPropAt_congr_of_eventuallyEq, liftPropAt_iff_comp_inclusion, liftPropAt_iff_comp_subtype_val, liftPropAt_of_liftPropWithinAt, liftPropAt_of_mem_groupoid, liftPropAt_of_mem_maximalAtlas, liftPropAt_symm_of_mem_maximalAtlas, liftPropOn_chart, liftPropOn_chart_symm, liftPropOn_congr, liftPropOn_congr_iff, liftPropOn_indep_chart, liftPropOn_mono, liftPropOn_of_liftProp, liftPropOn_of_locally_liftPropOn, liftPropOn_of_mem_groupoid, liftPropOn_of_mem_maximalAtlas, liftPropOn_symm_of_mem_maximalAtlas, liftPropWithinAt_congr, liftPropWithinAt_congr_iff, liftPropWithinAt_congr_iff_of_eventuallyEq, liftPropWithinAt_congr_iff_of_mem, liftPropWithinAt_congr_of_eventuallyEq, liftPropWithinAt_congr_of_eventuallyEq_of_mem, liftPropWithinAt_congr_of_mem, liftPropWithinAt_congr_set, liftPropWithinAt_iff, liftPropWithinAt_indep_chart, liftPropWithinAt_indep_chart', liftPropWithinAt_indep_chart_aux, liftPropWithinAt_indep_chart_source, liftPropWithinAt_indep_chart_source_aux, liftPropWithinAt_indep_chart_target, liftPropWithinAt_indep_chart_target_aux, liftPropWithinAt_indep_chart_target_aux2, liftPropWithinAt_inter, liftPropWithinAt_inter', liftPropWithinAt_mono, liftPropWithinAt_mono_of_mem_nhdsWithin, liftPropWithinAt_of_liftPropAt, liftPropWithinAt_of_liftPropAt_of_mem_nhds, liftProp_id, liftProp_inclusion, liftProp_of_locally_liftPropOn, liftProp_subtype_val, right_invariance, right_invariance', isLocalStructomorphWithinAt_localInvariantProp, liftPropOn_univ, liftPropWithinAt_self, liftPropWithinAt_self_source, liftPropWithinAt_self_target, liftPropWithinAt_univ	76
Total	82

ChartedSpace

Definitions

Name	Category	Theorems
LiftProp 📖	MathDef	7 math math: StructureGroupoid.LocalInvariantProp.liftProp_of_locally_liftPropOn, StructureGroupoid.LocalInvariantProp.liftProp_subtype_val, liftProp_iff, StructureGroupoid.LocalInvariantProp.section_spec, StructureGroupoid.LocalInvariantProp.liftProp_id, StructureGroupoid.LocalInvariantProp.liftProp_inclusion, StructureGroupoid.liftPropOn_univ
LiftPropAt 📖	MathDef	11 math math: StructureGroupoid.LocalInvariantProp.liftPropAt_of_liftPropWithinAt, StructureGroupoid.LocalInvariantProp.liftPropAt_chart_symm, StructureGroupoid.LocalInvariantProp.liftPropAt_of_mem_groupoid, liftPropAt_iff, StructureGroupoid.LocalInvariantProp.liftPropAt_congr_iff_of_eventuallyEq, StructureGroupoid.liftPropWithinAt_univ, StructureGroupoid.LocalInvariantProp.liftPropAt_symm_of_mem_maximalAtlas, StructureGroupoid.LocalInvariantProp.liftPropAt_iff_comp_subtype_val, StructureGroupoid.LocalInvariantProp.liftPropAt_of_mem_maximalAtlas, StructureGroupoid.LocalInvariantProp.liftPropAt_iff_comp_inclusion, StructureGroupoid.LocalInvariantProp.liftPropAt_chart
LiftPropOn 📖	MathDef	9 math math: isLocalStructomorphOn_contDiffGroupoid_iff, StructureGroupoid.LocalInvariantProp.liftPropOn_of_mem_groupoid, StructureGroupoid.LocalInvariantProp.liftPropOn_of_mem_maximalAtlas, StructureGroupoid.LocalInvariantProp.liftPropOn_of_liftProp, StructureGroupoid.LocalInvariantProp.liftPropOn_chart, StructureGroupoid.LocalInvariantProp.liftPropOn_symm_of_mem_maximalAtlas, StructureGroupoid.liftPropOn_univ, StructureGroupoid.LocalInvariantProp.liftPropOn_chart_symm, StructureGroupoid.LocalInvariantProp.liftPropOn_congr_iff
LiftPropWithinAt 📖	CompData	18 math math: StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart', StructureGroupoid.LocalInvariantProp.liftPropWithinAt_of_liftPropAt_of_mem_nhds, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_iff, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_iff_of_eventuallyEq, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_inter, StructureGroupoid.liftPropWithinAt_self_target, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_iff_of_mem, StructureGroupoid.liftPropWithinAt_univ, StructureGroupoid.liftPropWithinAt_self, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_of_liftPropAt, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_iff, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_source, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_target, StructureGroupoid.liftPropWithinAt_self_source, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_inter', StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_set, liftPropWithinAt_iff'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
liftPropAt_iff 📖	mathematical	—	LiftPropAt ContinuousAt OpenPartialHomeomorph.toFun' chartAt OpenPartialHomeomorph.symm Set.univ	—	LiftPropAt.eq_1 liftPropWithinAt_iff' continuousWithinAt_univ Set.preimage_univ
liftPropWithinAt_iff' 📖	mathematical	—	LiftPropWithinAt ContinuousWithinAt OpenPartialHomeomorph.toFun' chartAt OpenPartialHomeomorph.symm Set.preimage	—	—
liftProp_iff 📖	mathematical	—	LiftProp Continuous OpenPartialHomeomorph.toFun' chartAt OpenPartialHomeomorph.symm Set.univ	—	—

ChartedSpace.LiftPropWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousWithinAt 📖	mathematical	ChartedSpace.LiftPropWithinAt	ContinuousWithinAt	—	—
prop 📖	mathematical	ChartedSpace.LiftPropWithinAt	OpenPartialHomeomorph.toFun' chartAt OpenPartialHomeomorph.symm Set.preimage	—	—

OpenPartialHomeomorph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocalStructomorphWithinAt_iff 📖	mathematical	Set Set.instMembership Set.instUnion PartialEquiv.source toPartialEquiv Compl.compl Set.instCompl	StructureGroupoid.IsLocalStructomorphWithinAt toFun' OpenPartialHomeomorph StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid Set.instHasSubset Set.EqOn Set.instInter	—	closedUnderRestriction' open_source HasSubset.Subset.trans Set.instIsTransSubset Set.inter_subset_right interior_subset IsOpen.interior_eq
isLocalStructomorphWithinAt_iff' 📖	mathematical	Set Set.instHasSubset PartialEquiv.source toPartialEquiv Set.instMembership Set.instUnion Compl.compl Set.instCompl	StructureGroupoid.IsLocalStructomorphWithinAt toFun' OpenPartialHomeomorph StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid Set.EqOn	—	isLocalStructomorphWithinAt_iff Set.inter_eq_right HasSubset.Subset.trans Set.instIsTransSubset
isLocalStructomorphWithinAt_source_iff 📖	mathematical	—	StructureGroupoid.IsLocalStructomorphWithinAt toFun' PartialEquiv.source toPartialEquiv OpenPartialHomeomorph StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid Set Set.instHasSubset Set.EqOn Set.instMembership	—	isLocalStructomorphWithinAt_iff' Set.Subset.rfl Set.union_compl_self

StructureGroupoid

Definitions

Name	Category	Theorems
IsLocalStructomorphWithinAt 📖	MathDef	5 math math: OpenPartialHomeomorph.isLocalStructomorphWithinAt_iff, OpenPartialHomeomorph.isLocalStructomorphWithinAt_source_iff, isLocalStructomorphOn_contDiffGroupoid_iff, OpenPartialHomeomorph.isLocalStructomorphWithinAt_iff', isLocalStructomorphWithinAt_localInvariantProp
LocalInvariantProp 📖	CompData	4 math math: contDiffWithinAt_localInvariantProp, contDiffWithinAt_localInvariantProp_of_le, differentiableWithinAt_localInvariantProp, isLocalStructomorphWithinAt_localInvariantProp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocalStructomorphWithinAt_localInvariantProp 📖	mathematical	—	LocalInvariantProp IsLocalStructomorphWithinAt	—	Set.EqOn.mono closedUnderRestriction' isOpen_interior Set.ext IsOpen.interior_eq OpenPartialHomeomorph.left_inv trans symm
liftPropOn_univ 📖	mathematical	—	ChartedSpace.LiftPropOn Set.univ ChartedSpace.LiftProp	—	—
liftPropWithinAt_self 📖	mathematical	—	ChartedSpace.LiftPropWithinAt chartedSpaceSelf ContinuousWithinAt	—	ChartedSpace.liftPropWithinAt_iff'
liftPropWithinAt_self_source 📖	mathematical	—	ChartedSpace.LiftPropWithinAt chartedSpaceSelf ContinuousWithinAt OpenPartialHomeomorph.toFun' chartAt	—	ChartedSpace.liftPropWithinAt_iff'
liftPropWithinAt_self_target 📖	mathematical	—	ChartedSpace.LiftPropWithinAt chartedSpaceSelf ContinuousWithinAt OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm chartAt Set.preimage	—	ChartedSpace.liftPropWithinAt_iff'
liftPropWithinAt_univ 📖	mathematical	—	ChartedSpace.LiftPropWithinAt Set.univ ChartedSpace.LiftPropAt	—	—

StructureGroupoid.HasGroupoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	ChartedSpace.LiftPropOn StructureGroupoid.IsLocalStructomorphWithinAt OpenPartialHomeomorph.toFun' PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	HasGroupoid ChartedSpace.comp	—	StructureGroupoid.locality StructureGroupoid.LocalInvariantProp.liftPropOn_indep_chart StructureGroupoid.isLocalStructomorphWithinAt_localInvariantProp StructureGroupoid.subset_maximalAtlas StructureGroupoid.compatible OpenPartialHomeomorph.trans_assoc OpenPartialHomeomorph.open_source IsOpen.inter StructureGroupoid.mem_of_eqOnSource closedUnderRestriction' OpenPartialHomeomorph.restr_source_inter OpenPartialHomeomorph.Set.EqOn.restr_eqOn_source Set.EqOn.mono

StructureGroupoid.LocalInvariantProp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr' 📖	—	StructureGroupoid.LocalInvariantProp Filter.EventuallyEq nhds	—	—	congr Filter.EventuallyEq.symm
congr_iff 📖	—	StructureGroupoid.LocalInvariantProp Filter.EventuallyEq nhds	—	—	congr_iff_nhdsWithin mem_nhdsWithin_of_mem_nhds mem_of_mem_nhds
congr_iff_nhdsWithin 📖	—	StructureGroupoid.LocalInvariantProp Filter.EventuallyEq nhdsWithin	—	—	is_local_nhds congr_of_forall
congr_nhdsWithin 📖	—	StructureGroupoid.LocalInvariantProp Filter.EventuallyEq nhdsWithin	—	—	congr_iff_nhdsWithin
congr_nhdsWithin' 📖	—	StructureGroupoid.LocalInvariantProp Filter.EventuallyEq nhdsWithin	—	—	congr_iff_nhdsWithin
congr_of_forall 📖	—	StructureGroupoid.LocalInvariantProp	—	—	—
congr_set 📖	—	StructureGroupoid.LocalInvariantProp Filter.EventuallyEq nhds	—	—	mem_nhds_iff Filter.EventuallyEq.mem_iff is_local
is_local 📖	mathematical	StructureGroupoid.LocalInvariantProp IsOpen Set Set.instMembership	Set.instInter	—	—
is_local_nhds 📖	mathematical	StructureGroupoid.LocalInvariantProp Set Filter Filter.instMembership nhdsWithin	Set.instInter	—	congr_set mem_nhdsWithin_iff_eventuallyEq
left_invariance 📖	mathematical	StructureGroupoid.LocalInvariantProp OpenPartialHomeomorph StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid ContinuousWithinAt Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	OpenPartialHomeomorph.toFun'	—	ContinuousWithinAt.preimage_mem_nhdsWithin IsOpen.mem_nhds OpenPartialHomeomorph.open_source ContinuousAt.comp_continuousWithinAt OpenPartialHomeomorph.continuousAt OpenPartialHomeomorph.mapsTo left_invariance' StructureGroupoid.symm Set.inter_subset_right is_local_nhds congr_nhdsWithin Filter.eventually_of_mem OpenPartialHomeomorph.left_inv
left_invariance' 📖	mathematical	StructureGroupoid.LocalInvariantProp OpenPartialHomeomorph StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid Set Set.instHasSubset Set.preimage PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv Set.instMembership	OpenPartialHomeomorph.toFun'	—	—
liftPropAt_chart 📖	mathematical	StructureGroupoid.LocalInvariantProp Set.univ	ChartedSpace.LiftPropAt chartedSpaceSelf OpenPartialHomeomorph.toFun' chartAt	—	liftPropAt_of_mem_maximalAtlas StructureGroupoid.chart_mem_maximalAtlas mem_chart_source
liftPropAt_chart_symm 📖	mathematical	StructureGroupoid.LocalInvariantProp Set.univ	ChartedSpace.LiftPropAt chartedSpaceSelf OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm chartAt	—	liftPropAt_symm_of_mem_maximalAtlas StructureGroupoid.chart_mem_maximalAtlas
liftPropAt_congr_iff_of_eventuallyEq 📖	mathematical	StructureGroupoid.LocalInvariantProp Filter.EventuallyEq nhds	ChartedSpace.LiftPropAt	—	liftPropWithinAt_congr_iff_of_eventuallyEq nhdsWithin_univ Filter.EventuallyEq.eq_of_nhds
liftPropAt_congr_of_eventuallyEq 📖	—	StructureGroupoid.LocalInvariantProp ChartedSpace.LiftPropAt Filter.EventuallyEq nhds	—	—	liftPropAt_congr_iff_of_eventuallyEq
liftPropAt_iff_comp_inclusion 📖	mathematical	StructureGroupoid.LocalInvariantProp TopologicalSpace.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder	ChartedSpace.LiftPropAt SetLike.instMembership TopologicalSpace.Opens.instSetLike instTopologicalSpaceSubtype TopologicalSpace.Opens.instChartedSpace Set.inclusion SetLike.coe	—	SetLike.coe_subset_coe instIsConcreteLE Topology.IsOpenEmbedding.continuousAt_iff TopologicalSpace.Opens.isOpenEmbedding_of_le congr_iff Filter.EventuallyEq.fun_comp TopologicalSpace.Opens.chartAt_inclusion_symm_eventuallyEq
liftPropAt_iff_comp_subtype_val 📖	mathematical	StructureGroupoid.LocalInvariantProp	ChartedSpace.LiftPropAt TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike instTopologicalSpaceSubtype TopologicalSpace.Opens.instChartedSpace	—	Topology.IsOpenEmbedding.continuousAt_iff TopologicalSpace.Opens.isOpenEmbedding' congr_iff Filter.EventuallyEq.fun_comp TopologicalSpace.Opens.chartAt_subtype_val_symm_eventuallyEq
liftPropAt_of_liftPropWithinAt 📖	mathematical	StructureGroupoid.LocalInvariantProp ChartedSpace.LiftPropWithinAt Set Filter Filter.instMembership nhds	ChartedSpace.LiftPropAt	—	liftPropWithinAt_inter Set.univ_inter
liftPropAt_of_mem_groupoid 📖	mathematical	StructureGroupoid.LocalInvariantProp Set.univ OpenPartialHomeomorph StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	ChartedSpace.LiftPropAt chartedSpaceSelf OpenPartialHomeomorph.toFun'	—	liftPropAt_of_mem_maximalAtlas hasGroupoid_model_space StructureGroupoid.mem_maximalAtlas_of_mem_groupoid
liftPropAt_of_mem_maximalAtlas 📖	mathematical	StructureGroupoid.LocalInvariantProp Set.univ OpenPartialHomeomorph Set Set.instMembership StructureGroupoid.maximalAtlas PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	ChartedSpace.LiftPropAt chartedSpaceSelf OpenPartialHomeomorph.toFun'	—	liftPropWithinAt_indep_chart hasGroupoid_model_space StructureGroupoid.id_mem_maximalAtlas Set.mem_univ ContinuousAt.continuousWithinAt OpenPartialHomeomorph.continuousAt congr' OpenPartialHomeomorph.eventually_right_inverse'
liftPropAt_symm_of_mem_maximalAtlas 📖	mathematical	StructureGroupoid.LocalInvariantProp Set.univ OpenPartialHomeomorph Set Set.instMembership StructureGroupoid.maximalAtlas PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv	ChartedSpace.LiftPropAt chartedSpaceSelf OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm	—	congr' OpenPartialHomeomorph.eventually_right_inverse ChartedSpace.LiftPropAt.eq_1 liftPropWithinAt_indep_chart hasGroupoid_model_space StructureGroupoid.id_mem_maximalAtlas Set.mem_univ ContinuousAt.continuousWithinAt OpenPartialHomeomorph.continuousAt
liftPropOn_chart 📖	mathematical	StructureGroupoid.LocalInvariantProp Set.univ	ChartedSpace.LiftPropOn chartedSpaceSelf OpenPartialHomeomorph.toFun' chartAt PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	—	liftPropOn_of_mem_maximalAtlas StructureGroupoid.chart_mem_maximalAtlas
liftPropOn_chart_symm 📖	mathematical	StructureGroupoid.LocalInvariantProp Set.univ	ChartedSpace.LiftPropOn chartedSpaceSelf OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm chartAt PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv	—	liftPropOn_symm_of_mem_maximalAtlas StructureGroupoid.chart_mem_maximalAtlas
liftPropOn_congr 📖	—	StructureGroupoid.LocalInvariantProp ChartedSpace.LiftPropOn	—	—	liftPropWithinAt_congr
liftPropOn_congr_iff 📖	mathematical	StructureGroupoid.LocalInvariantProp	ChartedSpace.LiftPropOn	—	liftPropOn_congr
liftPropOn_indep_chart 📖	—	StructureGroupoid.LocalInvariantProp OpenPartialHomeomorph Set Set.instMembership StructureGroupoid.maximalAtlas ChartedSpace.LiftPropOn Set.instInter PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv Set.preimage OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm PartialEquiv.source	—	—	OpenPartialHomeomorph.right_inv liftPropWithinAt_indep_chart OpenPartialHomeomorph.symm_mapsTo
liftPropOn_mono 📖	—	ChartedSpace.LiftPropOn Set Set.instHasSubset	—	—	liftPropWithinAt_mono
liftPropOn_of_liftProp 📖	mathematical	ChartedSpace.LiftProp	ChartedSpace.LiftPropOn	—	liftPropOn_mono StructureGroupoid.liftPropOn_univ Set.subset_univ
liftPropOn_of_locally_liftPropOn 📖	—	StructureGroupoid.LocalInvariantProp IsOpen Set Set.instMembership ChartedSpace.LiftPropOn Set.instInter	—	—	liftPropWithinAt_inter IsOpen.mem_nhds
liftPropOn_of_mem_groupoid 📖	mathematical	StructureGroupoid.LocalInvariantProp Set.univ OpenPartialHomeomorph StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid	ChartedSpace.LiftPropOn chartedSpaceSelf OpenPartialHomeomorph.toFun' PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	—	liftPropOn_of_mem_maximalAtlas hasGroupoid_model_space StructureGroupoid.mem_maximalAtlas_of_mem_groupoid
liftPropOn_of_mem_maximalAtlas 📖	mathematical	StructureGroupoid.LocalInvariantProp Set.univ OpenPartialHomeomorph Set Set.instMembership StructureGroupoid.maximalAtlas	ChartedSpace.LiftPropOn chartedSpaceSelf OpenPartialHomeomorph.toFun' PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	—	liftPropWithinAt_of_liftPropAt_of_mem_nhds liftPropAt_of_mem_maximalAtlas IsOpen.mem_nhds OpenPartialHomeomorph.open_source
liftPropOn_symm_of_mem_maximalAtlas 📖	mathematical	StructureGroupoid.LocalInvariantProp Set.univ OpenPartialHomeomorph Set Set.instMembership StructureGroupoid.maximalAtlas	ChartedSpace.LiftPropOn chartedSpaceSelf OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv	—	liftPropWithinAt_of_liftPropAt_of_mem_nhds liftPropAt_symm_of_mem_maximalAtlas IsOpen.mem_nhds OpenPartialHomeomorph.open_target
liftPropWithinAt_congr 📖	—	StructureGroupoid.LocalInvariantProp ChartedSpace.LiftPropWithinAt	—	—	liftPropWithinAt_congr_iff
liftPropWithinAt_congr_iff 📖	mathematical	StructureGroupoid.LocalInvariantProp	ChartedSpace.LiftPropWithinAt	—	liftPropWithinAt_congr_iff_of_eventuallyEq eventually_nhdsWithin_of_forall
liftPropWithinAt_congr_iff_of_eventuallyEq 📖	mathematical	StructureGroupoid.LocalInvariantProp Filter.EventuallyEq nhdsWithin	ChartedSpace.LiftPropWithinAt	—	liftPropWithinAt_congr_of_eventuallyEq Filter.EventuallyEq.symm
liftPropWithinAt_congr_iff_of_mem 📖	mathematical	StructureGroupoid.LocalInvariantProp Set Set.instMembership	ChartedSpace.LiftPropWithinAt	—	liftPropWithinAt_congr_iff_of_eventuallyEq eventually_nhdsWithin_of_forall
liftPropWithinAt_congr_of_eventuallyEq 📖	—	StructureGroupoid.LocalInvariantProp ChartedSpace.LiftPropWithinAt Filter.EventuallyEq nhdsWithin	—	—	ContinuousWithinAt.congr_of_eventuallyEq ChartedSpace.LiftPropWithinAt.continuousWithinAt congr_nhdsWithin' OpenPartialHomeomorph.eventually_nhdsWithin' mem_chart_source Filter.Eventually.mono OpenPartialHomeomorph.left_inv ChartedSpace.LiftPropWithinAt.prop
liftPropWithinAt_congr_of_eventuallyEq_of_mem 📖	—	StructureGroupoid.LocalInvariantProp ChartedSpace.LiftPropWithinAt Filter.EventuallyEq nhdsWithin Set Set.instMembership	—	—	liftPropWithinAt_congr_of_eventuallyEq mem_of_mem_nhdsWithin
liftPropWithinAt_congr_of_mem 📖	—	StructureGroupoid.LocalInvariantProp ChartedSpace.LiftPropWithinAt Set Set.instMembership	—	—	liftPropWithinAt_congr_iff
liftPropWithinAt_congr_set 📖	mathematical	StructureGroupoid.LocalInvariantProp Filter.EventuallyEq nhds	ChartedSpace.LiftPropWithinAt	—	liftPropWithinAt_inter Set.ext
liftPropWithinAt_iff 📖	mathematical	StructureGroupoid.LocalInvariantProp	ChartedSpace.LiftPropWithinAt ContinuousWithinAt OpenPartialHomeomorph.toFun' chartAt OpenPartialHomeomorph.symm Set Set.instInter PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv Set.preimage PartialEquiv.source	—	ChartedSpace.liftPropWithinAt_iff' congr_set OpenPartialHomeomorph.preimage_eventuallyEq_target_inter_preimage_inter mem_chart_source chart_source_mem_nhds
liftPropWithinAt_indep_chart 📖	mathematical	StructureGroupoid.LocalInvariantProp OpenPartialHomeomorph Set Set.instMembership StructureGroupoid.maximalAtlas PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	ChartedSpace.LiftPropWithinAt ContinuousWithinAt OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm Set.preimage	—	liftPropWithinAt_indep_chart_aux StructureGroupoid.chart_mem_maximalAtlas mem_chart_source
liftPropWithinAt_indep_chart' 📖	mathematical	StructureGroupoid.LocalInvariantProp OpenPartialHomeomorph Set Set.instMembership StructureGroupoid.maximalAtlas PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	ChartedSpace.LiftPropWithinAt ContinuousWithinAt chartedSpaceSelf OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm Set.preimage	—	liftPropWithinAt_indep_chart StructureGroupoid.liftPropWithinAt_self OpenPartialHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_right OpenPartialHomeomorph.left_inv OpenPartialHomeomorph.continuousAt ContinuousAt.comp_continuousWithinAt
liftPropWithinAt_indep_chart_aux 📖	mathematical	StructureGroupoid.LocalInvariantProp OpenPartialHomeomorph Set Set.instMembership StructureGroupoid.maximalAtlas PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv ContinuousWithinAt	OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm Set.preimage	—	Function.comp_assoc liftPropWithinAt_indep_chart_source_aux liftPropWithinAt_indep_chart_target_aux
liftPropWithinAt_indep_chart_source 📖	mathematical	StructureGroupoid.LocalInvariantProp OpenPartialHomeomorph Set Set.instMembership StructureGroupoid.maximalAtlas PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	ChartedSpace.LiftPropWithinAt chartedSpaceSelf OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm Set.preimage	—	StructureGroupoid.liftPropWithinAt_self_source ChartedSpace.liftPropWithinAt_iff' OpenPartialHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_right OpenPartialHomeomorph.symm_symm OpenPartialHomeomorph.left_inv Function.comp_assoc liftPropWithinAt_indep_chart_source_aux StructureGroupoid.chart_mem_maximalAtlas mem_chart_source
liftPropWithinAt_indep_chart_source_aux 📖	mathematical	StructureGroupoid.LocalInvariantProp OpenPartialHomeomorph Set Set.instMembership StructureGroupoid.maximalAtlas PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm Set.preimage	—	right_invariance StructureGroupoid.compatible_of_mem_maximalAtlas OpenPartialHomeomorph.left_inv congr_iff Filter.Eventually.mono OpenPartialHomeomorph.eventually_nhds' OpenPartialHomeomorph.eventually_left_inverse congr_set Filter.Eventually.set_eq Filter.eventually_of_mem ContinuousAt.preimage_mem_nhds OpenPartialHomeomorph.continuousAt OpenPartialHomeomorph.mapsTo IsOpen.mem_nhds OpenPartialHomeomorph.open_source
liftPropWithinAt_indep_chart_target 📖	mathematical	StructureGroupoid.LocalInvariantProp OpenPartialHomeomorph Set Set.instMembership StructureGroupoid.maximalAtlas PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	ChartedSpace.LiftPropWithinAt ContinuousWithinAt chartedSpaceSelf OpenPartialHomeomorph.toFun'	—	StructureGroupoid.liftPropWithinAt_self_target ChartedSpace.liftPropWithinAt_iff' ContinuousAt.comp_continuousWithinAt OpenPartialHomeomorph.continuousAt liftPropWithinAt_indep_chart_target_aux mem_chart_source StructureGroupoid.chart_mem_maximalAtlas
liftPropWithinAt_indep_chart_target_aux 📖	mathematical	StructureGroupoid.LocalInvariantProp Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv OpenPartialHomeomorph StructureGroupoid.maximalAtlas ContinuousWithinAt	OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm Set.preimage	—	liftPropWithinAt_indep_chart_target_aux2 OpenPartialHomeomorph.left_inv ContinuousWithinAt.comp ContinuousAt.continuousWithinAt OpenPartialHomeomorph.continuousAt OpenPartialHomeomorph.mapsTo Set.Subset.rfl
liftPropWithinAt_indep_chart_target_aux2 📖	mathematical	StructureGroupoid.LocalInvariantProp OpenPartialHomeomorph Set Set.instMembership StructureGroupoid.maximalAtlas PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv ContinuousWithinAt	OpenPartialHomeomorph.toFun'	—	ContinuousAt.comp_continuousWithinAt OpenPartialHomeomorph.continuousAt left_invariance StructureGroupoid.compatible_of_mem_maximalAtlas OpenPartialHomeomorph.left_inv congr_iff_nhdsWithin Filter.Eventually.mono Filter.Tendsto.eventually OpenPartialHomeomorph.eventually_left_inverse
liftPropWithinAt_inter 📖	mathematical	StructureGroupoid.LocalInvariantProp Set Filter Filter.instMembership nhds	ChartedSpace.LiftPropWithinAt Set.instInter	—	liftPropWithinAt_inter' mem_nhdsWithin_of_mem_nhds
liftPropWithinAt_inter' 📖	mathematical	StructureGroupoid.LocalInvariantProp Set Filter Filter.instMembership nhdsWithin	ChartedSpace.LiftPropWithinAt Set.instInter	—	ChartedSpace.liftPropWithinAt_iff' continuousWithinAt_inter' congr_set OpenPartialHomeomorph.eventually_nhds' mem_chart_source Filter.EventuallyEq.mem_iff Filter.EventuallyEq.symm mem_nhdsWithin_iff_eventuallyEq
liftPropWithinAt_mono 📖	—	ChartedSpace.LiftPropWithinAt Set Set.instHasSubset	—	—	ContinuousWithinAt.mono ChartedSpace.LiftPropWithinAt.continuousWithinAt ChartedSpace.LiftPropWithinAt.prop
liftPropWithinAt_mono_of_mem_nhdsWithin 📖	—	ChartedSpace.LiftPropWithinAt Set Filter Filter.instMembership nhdsWithin	—	—	ContinuousWithinAt.mono_of_mem_nhdsWithin OpenPartialHomeomorph.map_nhdsWithin_preimage_eq mem_chart_target OpenPartialHomeomorph.left_inv mem_chart_source
liftPropWithinAt_of_liftPropAt 📖	mathematical	ChartedSpace.LiftPropAt	ChartedSpace.LiftPropWithinAt	—	liftPropWithinAt_mono StructureGroupoid.liftPropWithinAt_univ Set.subset_univ
liftPropWithinAt_of_liftPropAt_of_mem_nhds 📖	mathematical	StructureGroupoid.LocalInvariantProp ChartedSpace.LiftPropAt Set Filter Filter.instMembership nhds	ChartedSpace.LiftPropWithinAt	—	Set.univ_inter liftPropWithinAt_inter
liftProp_id 📖	mathematical	StructureGroupoid.LocalInvariantProp Set.univ	ChartedSpace.LiftProp	—	congr' OpenPartialHomeomorph.eventually_right_inverse mem_chart_target
liftProp_inclusion 📖	mathematical	StructureGroupoid.LocalInvariantProp Set.univ TopologicalSpace.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder	ChartedSpace.LiftProp SetLike.instMembership TopologicalSpace.Opens.instSetLike instTopologicalSpaceSubtype TopologicalSpace.Opens.instChartedSpace TopologicalSpace.Opens.inclusion	—	liftPropAt_iff_comp_inclusion liftProp_id
liftProp_of_locally_liftPropOn 📖	mathematical	StructureGroupoid.LocalInvariantProp IsOpen Set Set.instMembership ChartedSpace.LiftPropOn	ChartedSpace.LiftProp	—	StructureGroupoid.liftPropOn_univ liftPropOn_of_locally_liftPropOn Set.univ_inter
liftProp_subtype_val 📖	mathematical	StructureGroupoid.LocalInvariantProp Set.univ	ChartedSpace.LiftProp TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike instTopologicalSpaceSubtype TopologicalSpace.Opens.instChartedSpace	—	liftPropAt_iff_comp_subtype_val liftProp_id
right_invariance 📖	mathematical	StructureGroupoid.LocalInvariantProp OpenPartialHomeomorph StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm Set.preimage	—	right_invariance' StructureGroupoid.symm OpenPartialHomeomorph.mapsTo congr Filter.eventually_of_mem IsOpen.mem_nhds OpenPartialHomeomorph.open_source OpenPartialHomeomorph.left_inv congr_set Filter.eventuallyEq_set OpenPartialHomeomorph.symm_symm
right_invariance' 📖	mathematical	StructureGroupoid.LocalInvariantProp OpenPartialHomeomorph StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm Set.preimage	—	—

---

← Back to Index