Mathlib Map

Theorems · Theorem · general topology

OpenPartialHomeomorph.map_source

∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {x : X}, x ∈ e.source → ↑e x ∈ e.target
Defined in
Mathlib.Topology.OpenPartialHomeomorph.Defs
Cited by
21 results in Mathlib
Foundations
Depth 5 from the axioms · uses no axioms
Assumes
TopologicalSpaceTopologicalSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

OpenPartialHomeomorph.mapsTo · cited by 15OpenPartialHomeomorph.map…mem_chart_target · cited by 5mem_chart_targetOpenPartialHomeomorph.extend_image_target_mem_nhds · cited by 4OpenPartialHomeomorph.ext…OpenPartialHomeomorph.map_nhdsWithin_eq · cited by 4OpenPartialHomeomorph.map…OpenPartialHomeomorph.tendsto_symm · cited by 4OpenPartialHomeomorph.ten…OpenPartialHomeomorph.eventually_right_inverse' · cited by 3OpenPartialHomeomorph.eve…HasStrictFDerivAt.image_mem_toOpenPartialHomeomorph_target · cited by 3HasStrictFDerivAt.image_m…HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorphOfComplemented_target · cited by 2HasStrictFDerivAt.mem_imp…OpenPartialHomeomorph.symm_map_nhds_eq · cited by 2OpenPartialHomeomorph.sym…OpenPartialHomeomorph.map_nhdsWithin_preimage_eq · cited by 2OpenPartialHomeomorph.map…OpenPartialHomeomorph.hasFPowerSeriesAt_symm · cited by 2OpenPartialHomeomorph.has…OpenPartialHomeomorph.map_subtype_source · cited by 2OpenPartialHomeomorph.map…OpenPartialHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_left · cited by 2OpenPartialHomeomorph.con…IsLocalHomeomorph.existsUnique_continuousMap_lifts · cited by 2IsLocalHomeomorph.existsU…IsLocalHomeomorph.exists_lift_nhds · cited by 1IsLocalHomeomorph.exists_…Set · cited by 53352SetTopologicalSpace · cited by 24529TopologicalSpacePartialEquiv.source · cited by 964PartialEquiv.sourcePartialHomeomorph.toPartialEquiv · cited by 917PartialHomeomorph.toParti…OpenPartialHomeomorph.toPartialHomeomorph · cited by 851OpenPartialHomeomorph.toP…OpenPartialHomeomorph.toFun' · cited by 745OpenPartialHomeomorph.toF…OpenPartialHomeomorph · cited by 664OpenPartialHomeomorphPartialEquiv.target · cited by 650PartialEquiv.targetPartialEquiv.map_source' · cited by 9PartialEquiv.map_source'OpenPartialHomeomorph.map_sou…CITED BYCITES

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by21

Results whose statement or proof uses this declaration.