Loogle!

Result

Found 290 declarations mentioning OpenPartialHomeomorph.symm. Of these, only the first 200 are shown.

• OpenPartialHomeomorph.symm 📋 Mathlib.Topology.OpenPartialHomeomorph.Defs
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) : OpenPartialHomeomorph Y X
• OpenPartialHomeomorph.symm_bijective 📋 Mathlib.Topology.OpenPartialHomeomorph.Defs
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] : Function.Bijective OpenPartialHomeomorph.symm
• OpenPartialHomeomorph.symm_symm 📋 Mathlib.Topology.OpenPartialHomeomorph.Defs
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) : e.symm.symm = e
• OpenPartialHomeomorph.invFun_eq_coe 📋 Mathlib.Topology.OpenPartialHomeomorph.Defs
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) : e.invFun = ↑e.symm
• OpenPartialHomeomorph.coe_toPartialHomeomorph_symm 📋 Mathlib.Topology.OpenPartialHomeomorph.Defs
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) : ↑e.symm = ↑e.symm
• OpenPartialHomeomorph.continuousOn_symm 📋 Mathlib.Topology.OpenPartialHomeomorph.Defs
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) : ContinuousOn (↑e.symm) e.target
• OpenPartialHomeomorph.coe_coe_symm 📋 Mathlib.Topology.OpenPartialHomeomorph.Defs
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) : ↑e.symm = ↑e.symm
• OpenPartialHomeomorph.coe_toPartialEquiv_symm 📋 Mathlib.Topology.OpenPartialHomeomorph.Defs
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) : ↑e.symm = ↑e.symm
• OpenPartialHomeomorph.leftInvOn 📋 Mathlib.Topology.OpenPartialHomeomorph.Defs
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) : Set.LeftInvOn (↑e.symm) (↑e) e.source
• OpenPartialHomeomorph.rightInvOn 📋 Mathlib.Topology.OpenPartialHomeomorph.Defs
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) : Set.RightInvOn (↑e.symm) (↑e) e.target
• OpenPartialHomeomorph.symm_toPartialEquiv 📋 Mathlib.Topology.OpenPartialHomeomorph.Defs
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) : e.symm.toPartialEquiv = e.symm
• OpenPartialHomeomorph.symm_source 📋 Mathlib.Topology.OpenPartialHomeomorph.Defs
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) : e.symm.source = e.target
• OpenPartialHomeomorph.symm_target 📋 Mathlib.Topology.OpenPartialHomeomorph.Defs
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) : e.symm.target = e.source
• OpenPartialHomeomorph.mapsTo_symm 📋 Mathlib.Topology.OpenPartialHomeomorph.Defs
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) : Set.MapsTo (↑e.symm) e.target e.source
• OpenPartialHomeomorph.symm_mapsTo 📋 Mathlib.Topology.OpenPartialHomeomorph.Defs
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) : Set.MapsTo (↑e.symm) e.target e.source
• OpenPartialHomeomorph.left_inv 📋 Mathlib.Topology.OpenPartialHomeomorph.Defs
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (h : x ∈ e.source) : ↑e.symm (↑e x) = x
• OpenPartialHomeomorph.right_inv 📋 Mathlib.Topology.OpenPartialHomeomorph.Defs
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : Y} (h : x ∈ e.target) : ↑e (↑e.symm x) = x
• Homeomorph.toOpenPartialHomeomorph_symm_apply 📋 Mathlib.Topology.OpenPartialHomeomorph.Defs
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) : ↑e.toOpenPartialHomeomorph.symm = ⇑e.symm
• OpenPartialHomeomorph.invOn 📋 Mathlib.Topology.OpenPartialHomeomorph.Defs
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) : Set.InvOn (↑e.symm) (↑e) e.source e.target
• OpenPartialHomeomorph.map_target 📋 Mathlib.Topology.OpenPartialHomeomorph.Defs
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : Y} (h : x ∈ e.target) : ↑e.symm x ∈ e.source
• OpenPartialHomeomorph.eq_symm_apply 📋 Mathlib.Topology.OpenPartialHomeomorph.Defs
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} {y : Y} (hx : x ∈ e.source) (hy : y ∈ e.target) : x = ↑e.symm y ↔ ↑e x = y
• OpenPartialHomeomorph.ext 📋 Mathlib.Topology.OpenPartialHomeomorph.Defs
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e e' : OpenPartialHomeomorph X Y) (h : ∀ (x : X), ↑e x = ↑e' x) (hinv : ∀ (x : Y), ↑e.symm x = ↑e'.symm x) (hs : e.source = e'.source) : e = e'
• Homeomorph.toOpenPartialHomeomorphOfImageEq_symm_apply 📋 Mathlib.Topology.OpenPartialHomeomorph.Defs
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) (s : Set X) (hs : IsOpen s) (t : Set Y) (h : ⇑e '' s = t) : ↑(e.toOpenPartialHomeomorphOfImageEq s hs t h).symm = ⇑e.symm
• OpenPartialHomeomorph.ext_iff 📋 Mathlib.Topology.OpenPartialHomeomorph.Defs
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e e' : OpenPartialHomeomorph X Y} : e = e' ↔ (∀ (x : X), ↑e x = ↑e' x) ∧ (∀ (x : Y), ↑e.symm x = ↑e'.symm x) ∧ e.source = e'.source
• OpenPartialHomeomorph.coe_mk_symm 📋 Mathlib.Topology.OpenPartialHomeomorph.Defs
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialEquiv X Y) (h₁ : ContinuousOn (↑e) e.source) (h₂ : ContinuousOn e.invFun e.target) (h₃ : IsOpen { toPartialEquiv := e, continuousOn_toFun := h₁, continuousOn_invFun := h₂ }.source) (h₄ : IsOpen { toPartialEquiv := e, continuousOn_toFun := h₁, continuousOn_invFun := h₂ }.target) : ↑{ toPartialEquiv := e, continuousOn_toFun := h₁, continuousOn_invFun := h₂, open_source := h₃, open_target := h₄ }.symm = ↑e.symm
• OpenPartialHomeomorph.mk_coe_symm 📋 Mathlib.Topology.OpenPartialHomeomorph.Defs
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialEquiv X Y) (h₁ : ContinuousOn (↑e) e.source) (h₂ : ContinuousOn e.invFun e.target) (h₃ : IsOpen { toPartialEquiv := e, continuousOn_toFun := h₁, continuousOn_invFun := h₂ }.source) (h₄ : IsOpen { toPartialEquiv := e, continuousOn_toFun := h₁, continuousOn_invFun := h₂ }.target) : ↑{ toPartialEquiv := e, continuousOn_toFun := h₁, continuousOn_invFun := h₂, open_source := h₃, open_target := h₄ }.symm = ↑e.symm
• AddCircle.openPartialHomeomorphCoe_symm_apply 📋 Mathlib.Topology.Instances.AddCircle.Defs
  {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [DiscreteTopology ↥(AddSubgroup.zmultiples p)] (x : AddCircle p) : ↑(AddCircle.openPartialHomeomorphCoe p a).symm x = ↑((AddCircle.equivIco p a) x)
• OpenPartialHomeomorph.refl_symm 📋 Mathlib.Topology.OpenPartialHomeomorph.Basic
  {X : Type u_1} [TopologicalSpace X] : (OpenPartialHomeomorph.refl X).symm = OpenPartialHomeomorph.refl X
• Topology.IsOpenEmbedding.toOpenPartialHomeomorph_left_inv 📋 Mathlib.Topology.OpenPartialHomeomorph.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (h : Topology.IsOpenEmbedding f) [Nonempty X] {x : X} : ↑(Topology.IsOpenEmbedding.toOpenPartialHomeomorph f h).symm (f x) = x
• Topology.IsOpenEmbedding.toOpenPartialHomeomorph_right_inv 📋 Mathlib.Topology.OpenPartialHomeomorph.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (h : Topology.IsOpenEmbedding f) [Nonempty X] {x : Y} (hx : x ∈ Set.range f) : f (↑(Topology.IsOpenEmbedding.toOpenPartialHomeomorph f h).symm x) = x
• OpenPartialHomeomorph.isOpen_inter_preimage_symm 📋 Mathlib.Topology.OpenPartialHomeomorph.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : Set X} (hs : IsOpen s) : IsOpen (e.target ∩ ↑e.symm ⁻¹' s)
• OpenPartialHomeomorph.isOpen_image_symm_of_subset_target 📋 Mathlib.Topology.OpenPartialHomeomorph.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {t : Set Y} (ht : IsOpen t) (hte : t ⊆ e.target) : IsOpen (↑e.symm '' t)
• OpenPartialHomeomorph.isOpen_symm_image_iff_of_subset_target 📋 Mathlib.Topology.OpenPartialHomeomorph.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {t : Set Y} (hs : t ⊆ e.target) : IsOpen (↑e.symm '' t) ↔ IsOpen t
• OpenPartialHomeomorph.symm_image_target_eq_source 📋 Mathlib.Topology.OpenPartialHomeomorph.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) : ↑e.symm '' e.target = e.source
• OpenPartialHomeomorph.coe_ofContinuousOpen_symm 📋 Mathlib.Topology.OpenPartialHomeomorph.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialEquiv X Y) (hc : ContinuousOn (↑e) e.source) (ho : IsOpenMap ↑e) (hs : IsOpen e.source) : ↑(OpenPartialHomeomorph.ofContinuousOpen e hc ho hs).symm = ↑e.symm
• OpenPartialHomeomorph.image_source_inter_eq' 📋 Mathlib.Topology.OpenPartialHomeomorph.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) : ↑e '' (e.source ∩ s) = e.target ∩ ↑e.symm ⁻¹' s
• OpenPartialHomeomorph.source_inter_preimage_inv_preimage 📋 Mathlib.Topology.OpenPartialHomeomorph.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) : e.source ∩ ↑e ⁻¹' ↑e.symm ⁻¹' s = e.source ∩ s
• OpenPartialHomeomorph.target_inter_inv_preimage_preimage 📋 Mathlib.Topology.OpenPartialHomeomorph.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set Y) : e.target ∩ ↑e.symm ⁻¹' ↑e ⁻¹' s = e.target ∩ s
• OpenPartialHomeomorph.image_eq_target_inter_inv_preimage 📋 Mathlib.Topology.OpenPartialHomeomorph.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : Set X} (h : s ⊆ e.source) : ↑e '' s = e.target ∩ ↑e.symm ⁻¹' s
• OpenPartialHomeomorph.symm_image_eq_source_inter_preimage 📋 Mathlib.Topology.OpenPartialHomeomorph.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : Set Y} (h : s ⊆ e.target) : ↑e.symm '' s = e.source ∩ ↑e ⁻¹' s
• OpenPartialHomeomorph.coe_ofContinuousOpenRestrict_symm 📋 Mathlib.Topology.OpenPartialHomeomorph.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialEquiv X Y) (hc : ContinuousOn (↑e) e.source) (ho : IsOpenMap (e.source.domRestrict ↑e)) (hs : IsOpen e.source) : ↑(OpenPartialHomeomorph.ofContinuousOpenRestrict e hc ho hs).symm = ↑e.symm
• OpenPartialHomeomorph.image_source_inter_eq 📋 Mathlib.Topology.OpenPartialHomeomorph.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) : ↑e '' (e.source ∩ s) = e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s)
• OpenPartialHomeomorph.symm_image_target_inter_eq 📋 Mathlib.Topology.OpenPartialHomeomorph.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set Y) : ↑e.symm '' (e.target ∩ s) = e.source ∩ ↑e ⁻¹' (e.target ∩ s)
• OpenPartialHomeomorph.toHomeomorphOfSourceEqUnivTargetEqUniv_symm_apply 📋 Mathlib.Topology.OpenPartialHomeomorph.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (h : e.source = Set.univ) (h' : e.target = Set.univ) : ⇑(e.toHomeomorphOfSourceEqUnivTargetEqUniv h h').symm = ↑e.symm
• OpenPartialHomeomorph.homeomorphOfImageSubsetSource_symm_apply_coe 📋 Mathlib.Topology.OpenPartialHomeomorph.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : Set X} {t : Set Y} (hs : s ⊆ e.source) (ht : ↑e '' s = t) (a✝ : ↑t) : ↑((e.homeomorphOfImageSubsetSource hs ht).symm a✝) = ↑e.symm ↑a✝
• OpenPartialHomeomorph.toHomeomorphSourceTarget_symm_apply_coe 📋 Mathlib.Topology.OpenPartialHomeomorph.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (a✝ : ↑e.target) : ↑(e.toHomeomorphSourceTarget.symm a✝) = ↑e.symm ↑a✝
• OpenPartialHomeomorph.continuousAt_symm 📋 Mathlib.Topology.OpenPartialHomeomorph.Continuity
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : Y} (h : x ∈ e.target) : ContinuousAt (↑e.symm) x
• OpenPartialHomeomorph.eventually_left_inverse 📋 Mathlib.Topology.OpenPartialHomeomorph.Continuity
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (hx : x ∈ e.source) : ∀ᶠ (y : X) in nhds x, ↑e.symm (↑e y) = y
• OpenPartialHomeomorph.eventually_right_inverse 📋 Mathlib.Topology.OpenPartialHomeomorph.Continuity
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : Y} (hx : x ∈ e.target) : ∀ᶠ (y : Y) in nhds x, ↑e (↑e.symm y) = y
• OpenPartialHomeomorph.tendsto_symm 📋 Mathlib.Topology.OpenPartialHomeomorph.Continuity
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (hx : x ∈ e.source) : Filter.Tendsto (↑e.symm) (nhds (↑e x)) (nhds x)
• OpenPartialHomeomorph.symm_map_nhds_eq 📋 Mathlib.Topology.OpenPartialHomeomorph.Continuity
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (hx : x ∈ e.source) : Filter.map (↑e.symm) (nhds (↑e x)) = nhds x
• OpenPartialHomeomorph.eventually_right_inverse' 📋 Mathlib.Topology.OpenPartialHomeomorph.Continuity
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (hx : x ∈ e.source) : ∀ᶠ (y : Y) in nhds (↑e x), ↑e (↑e.symm y) = y
• OpenPartialHomeomorph.eventually_nhds' 📋 Mathlib.Topology.OpenPartialHomeomorph.Continuity
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (p : X → Prop) (hx : x ∈ e.source) : (∀ᶠ (y : Y) in nhds (↑e x), p (↑e.symm y)) ↔ ∀ᶠ (x : X) in nhds x, p x
• OpenPartialHomeomorph.eventually_left_inverse' 📋 Mathlib.Topology.OpenPartialHomeomorph.Continuity
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : Y} (hx : x ∈ e.target) : ∀ᶠ (y : X) in nhds (↑e.symm x), ↑e.symm (↑e y) = y
• OpenPartialHomeomorph.continuousAt_iff_continuousAt_comp_right 📋 Mathlib.Topology.OpenPartialHomeomorph.Continuity
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) {f : Y → Z} {x : Y} (h : x ∈ e.target) : ContinuousAt f x ↔ ContinuousAt (f ∘ ↑e) (↑e.symm x)
• OpenPartialHomeomorph.eventually_nhdsWithin 📋 Mathlib.Topology.OpenPartialHomeomorph.Continuity
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (p : Y → Prop) {s : Set X} (hx : x ∈ e.source) : (∀ᶠ (y : Y) in nhdsWithin (↑e x) (↑e.symm ⁻¹' s), p y) ↔ ∀ᶠ (x : X) in nhdsWithin x s, p (↑e x)
• OpenPartialHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_right 📋 Mathlib.Topology.OpenPartialHomeomorph.Continuity
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) {f : Y → Z} {s : Set Y} {x : Y} (h : x ∈ e.target) : ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ∘ ↑e) (↑e ⁻¹' s) (↑e.symm x)
• OpenPartialHomeomorph.eventually_nhdsWithin' 📋 Mathlib.Topology.OpenPartialHomeomorph.Continuity
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (p : X → Prop) {s : Set X} (hx : x ∈ e.source) : (∀ᶠ (y : Y) in nhdsWithin (↑e x) (↑e.symm ⁻¹' s), p (↑e.symm y)) ↔ ∀ᶠ (x : X) in nhdsWithin x s, p x
• OpenPartialHomeomorph.preimage_eventuallyEqSet_target_inter_preimage_inter 📋 Mathlib.Topology.OpenPartialHomeomorph.Continuity
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Z} {x : X} {f : X → Z} (hf : ContinuousWithinAt f s x) (hxe : x ∈ e.source) (ht : t ∈ nhds (f x)) : ↑e.symm ⁻¹' s =ᶠ[nhds (↑e x)] e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' t)
• OpenPartialHomeomorph.preimage_eventuallyEq_target_inter_preimage_inter 📋 Mathlib.Topology.OpenPartialHomeomorph.Continuity
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Z} {x : X} {f : X → Z} (hf : ContinuousWithinAt f s x) (hxe : x ∈ e.source) (ht : t ∈ nhds (f x)) : ↑e.symm ⁻¹' s =ᶠ[nhds (↑e x)] e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' t)
• OpenPartialHomeomorph.isBigO_congr 📋 Mathlib.Analysis.Asymptotics.Lemmas
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {E : Type u_3} [Norm E] {F : Type u_4} [Norm F] (e : OpenPartialHomeomorph α β) {b : β} (hb : b ∈ e.target) {f : β → E} {g : β → F} : f =O[nhds b] g ↔ (f ∘ ↑e) =O[nhds (↑e.symm b)] (g ∘ ↑e)
• OpenPartialHomeomorph.isLittleO_congr 📋 Mathlib.Analysis.Asymptotics.Lemmas
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {E : Type u_3} [Norm E] {F : Type u_4} [Norm F] (e : OpenPartialHomeomorph α β) {b : β} (hb : b ∈ e.target) {f : β → E} {g : β → F} : f =o[nhds b] g ↔ (f ∘ ↑e) =o[nhds (↑e.symm b)] (g ∘ ↑e)
• OpenPartialHomeomorph.isBigOWith_congr 📋 Mathlib.Analysis.Asymptotics.Lemmas
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {E : Type u_3} [Norm E] {F : Type u_4} [Norm F] (e : OpenPartialHomeomorph α β) {b : β} (hb : b ∈ e.target) {f : β → E} {g : β → F} {C : ℝ} : Asymptotics.IsBigOWith C (nhds b) f g ↔ Asymptotics.IsBigOWith C (nhds (↑e.symm b)) (f ∘ ↑e) (g ∘ ↑e)
• Real.expPartialHomeomorph_symm_apply 📋 Mathlib.Analysis.SpecialFunctions.Log.Basic
  (x : ℝ) : ↑Real.expPartialHomeomorph.symm x = Real.log x
• OpenPartialHomeomorph.hasFPowerSeriesAt_symm 📋 Mathlib.Analysis.Analytic.Inverse
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : OpenPartialHomeomorph E F) {a : E} {i : E ≃L[𝕜] F} (h0 : a ∈ f.source) {p : FormalMultilinearSeries 𝕜 E F} (h : HasFPowerSeriesAt (↑f) p a) (hp : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i) : HasFPowerSeriesAt (↑f.symm) (p.leftInv i a) (↑f a)
• OpenPartialHomeomorph.analyticAt_symm' 📋 Mathlib.Analysis.Calculus.FDeriv.Analytic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : OpenPartialHomeomorph E F) {a : E} {i : E ≃L[𝕜] F} (h0 : a ∈ f.source) (h : AnalyticAt 𝕜 (↑f) a) (h' : fderiv 𝕜 (↑f) a = ↑i) : AnalyticAt 𝕜 (↑f.symm) (↑f a)
• OpenPartialHomeomorph.analyticAt_symm 📋 Mathlib.Analysis.Calculus.FDeriv.Analytic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : OpenPartialHomeomorph E F) {a : F} {i : E ≃L[𝕜] F} (h0 : a ∈ f.target) (h : AnalyticAt 𝕜 (↑f) (↑f.symm a)) (h' : fderiv 𝕜 (↑f) (↑f.symm a) = ↑i) : AnalyticAt 𝕜 (↑f.symm) a
• OpenPartialHomeomorph.hasFDerivAt_symm 📋 Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : OpenPartialHomeomorph E F) {f' : E ≃L[𝕜] F} {a : F} (ha : a ∈ f.target) (htff' : HasFDerivAt (↑f) (↑f') (↑f.symm a)) : HasFDerivAt (↑f.symm) (↑f'.symm) a
• OpenPartialHomeomorph.hasStrictFDerivAt_symm 📋 Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : OpenPartialHomeomorph E F) {f' : E ≃L[𝕜] F} {a : F} (ha : a ∈ f.target) (htff' : HasStrictFDerivAt (↑f) (↑f') (↑f.symm a)) : HasStrictFDerivAt (↑f.symm) (↑f'.symm) a
• OpenPartialHomeomorph.hasDerivAt_symm 📋 Mathlib.Analysis.Calculus.Deriv.Inverse
  {𝕜 : Type u} [NontriviallyNormedField 𝕜] (f : OpenPartialHomeomorph 𝕜 𝕜) {a f' : 𝕜} (ha : a ∈ f.target) (hf' : f' ≠ 0) (htff' : HasDerivAt (↑f) f' (↑f.symm a)) : HasDerivAt (↑f.symm) f'⁻¹ a
• OpenPartialHomeomorph.hasStrictDerivAt_symm 📋 Mathlib.Analysis.Calculus.Deriv.Inverse
  {𝕜 : Type u} [NontriviallyNormedField 𝕜] (f : OpenPartialHomeomorph 𝕜 𝕜) {a f' : 𝕜} (ha : a ∈ f.target) (hf' : f' ≠ 0) (htff' : HasStrictDerivAt (↑f) f' (↑f.symm a)) : HasStrictDerivAt (↑f.symm) f'⁻¹ a
• OpenPartialHomeomorph.ofSet_symm 📋 Mathlib.Topology.OpenPartialHomeomorph.IsImage
  {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsOpen s) : (OpenPartialHomeomorph.ofSet s hs).symm = OpenPartialHomeomorph.ofSet s hs
• OpenPartialHomeomorph.IsImage.symm 📋 Mathlib.Topology.OpenPartialHomeomorph.IsImage
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) : e.symm.IsImage t s
• OpenPartialHomeomorph.IsImage.symm_iff 📋 Mathlib.Topology.OpenPartialHomeomorph.IsImage
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} : e.symm.IsImage t s ↔ e.IsImage s t
• Homeomorph.symm_toOpenPartialHomeomorph 📋 Mathlib.Topology.OpenPartialHomeomorph.IsImage
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) : e.symm.toOpenPartialHomeomorph = e.toOpenPartialHomeomorph.symm
• OpenPartialHomeomorph.restr_symm_apply 📋 Mathlib.Topology.OpenPartialHomeomorph.IsImage
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) : ↑(e.restr s).symm = ↑e.symm
• OpenPartialHomeomorph.coe_restrOpen_symm 📋 Mathlib.Topology.OpenPartialHomeomorph.IsImage
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : Set X} (hs : IsOpen s) : ↑(e.restrOpen s hs).symm = ↑e.symm
• OpenPartialHomeomorph.EqOnSource.symm' 📋 Mathlib.Topology.OpenPartialHomeomorph.IsImage
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {e e' : OpenPartialHomeomorph X Y} (h : e ≈ e') : e.symm ≈ e'.symm
• OpenPartialHomeomorph.restr_target 📋 Mathlib.Topology.OpenPartialHomeomorph.IsImage
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) : (e.restr s).target = e.target ∩ ↑e.symm ⁻¹' interior s
• OpenPartialHomeomorph.IsImage.symm_apply_mem_iff 📋 Mathlib.Topology.OpenPartialHomeomorph.IsImage
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {y : Y} (h : e.IsImage s t) (hy : y ∈ e.target) : ↑e.symm y ∈ s ↔ y ∈ t
• OpenPartialHomeomorph.EqOnSource.symm_eqOn_target 📋 Mathlib.Topology.OpenPartialHomeomorph.IsImage
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {e e' : OpenPartialHomeomorph X Y} (h : e ≈ e') : Set.EqOn (↑e.symm) (↑e'.symm) e.target
• OpenPartialHomeomorph.IsImage.symm_mapsTo 📋 Mathlib.Topology.OpenPartialHomeomorph.IsImage
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) : Set.MapsTo (↑e.symm) (e.target ∩ t) (e.source ∩ s)
• OpenPartialHomeomorph.IsImage.of_symm_image_eq 📋 Mathlib.Topology.OpenPartialHomeomorph.IsImage
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : ↑e.symm '' (e.target ∩ t) = e.source ∩ s) : e.IsImage s t
• OpenPartialHomeomorph.IsImage.of_symm_preimage_eq 📋 Mathlib.Topology.OpenPartialHomeomorph.IsImage
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} : e.target ∩ ↑e.symm ⁻¹' s = e.target ∩ t → e.IsImage s t
• OpenPartialHomeomorph.IsImage.restr_symm_apply 📋 Mathlib.Topology.OpenPartialHomeomorph.IsImage
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) (hs : IsOpen (e.source ∩ s)) : ↑(h.restr hs).symm = ↑e.symm
• OpenPartialHomeomorph.IsImage.symm_image_eq 📋 Mathlib.Topology.OpenPartialHomeomorph.IsImage
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) : ↑e.symm '' (e.target ∩ t) = e.source ∩ s
• OpenPartialHomeomorph.IsImage.symm_preimage_eq 📋 Mathlib.Topology.OpenPartialHomeomorph.IsImage
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} : e.IsImage s t → e.target ∩ ↑e.symm ⁻¹' s = e.target ∩ t
• OpenPartialHomeomorph.IsImage.iff_symm_preimage_eq 📋 Mathlib.Topology.OpenPartialHomeomorph.IsImage
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} : e.IsImage s t ↔ e.target ∩ ↑e.symm ⁻¹' s = e.target ∩ t
• OpenPartialHomeomorph.IsImage.of_symm_preimage_eq' 📋 Mathlib.Topology.OpenPartialHomeomorph.IsImage
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} : e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s) = e.target ∩ t → e.IsImage s t
• OpenPartialHomeomorph.IsImage.symm_preimage_eq' 📋 Mathlib.Topology.OpenPartialHomeomorph.IsImage
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} : e.IsImage s t → e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s) = e.target ∩ t
• OpenPartialHomeomorph.IsImage.iff_symm_preimage_eq' 📋 Mathlib.Topology.OpenPartialHomeomorph.IsImage
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} : e.IsImage s t ↔ e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s) = e.target ∩ t
• OpenPartialHomeomorph.IsImage.leftInvOn_piecewise 📋 Mathlib.Topology.OpenPartialHomeomorph.IsImage
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {e' : OpenPartialHomeomorph X Y} [(i : X) → Decidable (i ∈ s)] [(i : Y) → Decidable (i ∈ t)] (h : e.IsImage s t) (h' : e'.IsImage s t) : Set.LeftInvOn (t.piecewise ↑e.symm ↑e'.symm) (s.piecewise ↑e ↑e') (s.ite e.source e'.source)
• OpenPartialHomeomorph.IsImage.symm_eqOn_of_inter_eq_of_eqOn 📋 Mathlib.Topology.OpenPartialHomeomorph.IsImage
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {e' : OpenPartialHomeomorph X Y} (h : e.IsImage s t) (hs : e.source ∩ s = e'.source ∩ s) (Heq : Set.EqOn (↑e) (↑e') (e.source ∩ s)) : Set.EqOn (↑e.symm) (↑e'.symm) (e.target ∩ t)
• OpenPartialHomeomorph.restrContDiff_symm_apply 📋 Mathlib.Analysis.Calculus.ContDiff.Operations
  (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : OpenPartialHomeomorph E F) (n : WithTop ℕ∞) (hn : n ≠ ↑⊤) (a✝ : F) : ↑(OpenPartialHomeomorph.restrContDiff 𝕜 f n hn).symm a✝ = ↑f.symm a✝
• OpenPartialHomeomorph.contDiffOn_restrContDiff_target 📋 Mathlib.Analysis.Calculus.ContDiff.Operations
  (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : OpenPartialHomeomorph E F) {n : WithTop ℕ∞} (hn : n ≠ ↑⊤) : ContDiffOn 𝕜 n (↑f.symm) (OpenPartialHomeomorph.restrContDiff 𝕜 f n hn).target
• OpenPartialHomeomorph.restrContDiff_source 📋 Mathlib.Analysis.Calculus.ContDiff.Operations
  (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : OpenPartialHomeomorph E F) (n : WithTop ℕ∞) (hn : n ≠ ↑⊤) : (OpenPartialHomeomorph.restrContDiff 𝕜 f n hn).source = f.source ∩ {x | ContDiffAt 𝕜 n (↑f) x ∧ ContDiffAt 𝕜 n (↑f.symm) (↑f x)}
• OpenPartialHomeomorph.restrContDiff_target 📋 Mathlib.Analysis.Calculus.ContDiff.Operations
  (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : OpenPartialHomeomorph E F) (n : WithTop ℕ∞) (hn : n ≠ ↑⊤) : (OpenPartialHomeomorph.restrContDiff 𝕜 f n hn).target = f.target ∩ {y | ContDiffAt 𝕜 n (↑f.symm) y ∧ ContDiffAt 𝕜 n (↑f) (↑f.symm y)}
• OpenPartialHomeomorph.contDiffAt_symm_deriv 📋 Mathlib.Analysis.Calculus.ContDiff.Operations
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} [CompleteSpace 𝕜] (f : OpenPartialHomeomorph 𝕜 𝕜) {f₀' a : 𝕜} (h₀ : f₀' ≠ 0) (ha : a ∈ f.target) (hf₀' : HasDerivAt (↑f) f₀' (↑f.symm a)) (hf : ContDiffAt 𝕜 n (↑f) (↑f.symm a)) : ContDiffAt 𝕜 n (↑f.symm) a
• OpenPartialHomeomorph.contDiffAt_symm 📋 Mathlib.Analysis.Calculus.ContDiff.Operations
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} [CompleteSpace E] (f : OpenPartialHomeomorph E F) {f₀' : E ≃L[𝕜] F} {a : F} (ha : a ∈ f.target) (hf₀' : HasFDerivAt (↑f) (↑f₀') (↑f.symm a)) (hf : ContDiffAt 𝕜 n (↑f) (↑f.symm a)) : ContDiffAt 𝕜 n (↑f.symm) a
• HasStrictFDerivAt.localInverse_def 📋 Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} [CompleteSpace E] (hf : HasStrictFDerivAt f (↑f') a) : HasStrictFDerivAt.localInverse f f' a hf = ↑(HasStrictFDerivAt.toOpenPartialHomeomorph f hf).symm
• OpenPartialHomeomorph.trans_symm_eq_symm_trans_symm 📋 Mathlib.Topology.OpenPartialHomeomorph.Composition
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) : (e.trans e').symm = e'.symm.trans e.symm
• OpenPartialHomeomorph.self_trans_symm 📋 Mathlib.Topology.OpenPartialHomeomorph.Composition
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) : e.trans e.symm ≈ OpenPartialHomeomorph.ofSet e.source ⋯
• OpenPartialHomeomorph.symm_trans_self 📋 Mathlib.Topology.OpenPartialHomeomorph.Composition
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) : e.symm.trans e ≈ OpenPartialHomeomorph.ofSet e.target ⋯
• OpenPartialHomeomorph.coe_trans_symm 📋 Mathlib.Topology.OpenPartialHomeomorph.Composition
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) : ↑(e.trans e').symm = ↑e.symm ∘ ↑e'.symm
• Homeomorph.transOpenPartialHomeomorph_symm_apply 📋 Mathlib.Topology.OpenPartialHomeomorph.Composition
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : X ≃ₜ Y) (f' : OpenPartialHomeomorph Y Z) : ↑(e.transOpenPartialHomeomorph f').symm = ⇑e.symm ∘ ↑f'.symm
• OpenPartialHomeomorph.inv_image_trans_target 📋 Mathlib.Topology.OpenPartialHomeomorph.Composition
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) : ↑e'.symm '' (e.trans e').target = e'.source ∩ e.target
• OpenPartialHomeomorph.trans_source'' 📋 Mathlib.Topology.OpenPartialHomeomorph.Composition
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) : (e.trans e').source = ↑e.symm '' (e.target ∩ e'.source)
• OpenPartialHomeomorph.trans_target 📋 Mathlib.Topology.OpenPartialHomeomorph.Composition
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) : (e.trans e').target = e'.target ∩ ↑e'.symm ⁻¹' e.target
• OpenPartialHomeomorph.trans'_symm_apply 📋 Mathlib.Topology.OpenPartialHomeomorph.Composition
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) (h : e.target = e'.source) (a✝ : Z) : ↑(e.trans' e' h).symm a✝ = ↑e.symm (↑e'.symm a✝)
• OpenPartialHomeomorph.trans_target' 📋 Mathlib.Topology.OpenPartialHomeomorph.Composition
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) : (e.trans e').target = e'.target ∩ ↑e'.symm ⁻¹' (e'.source ∩ e.target)
• OpenPartialHomeomorph.symm_trans_restr 📋 Mathlib.Topology.OpenPartialHomeomorph.Composition
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : Set X} (e' : OpenPartialHomeomorph X Y) (hs : IsOpen s) : e'.symm.trans (e.restr s) ≈ (e'.symm.trans e).restr (e'.target ∩ ↑e'.symm ⁻¹' s)
• OpenPartialHomeomorph.restr_symm_trans 📋 Mathlib.Topology.OpenPartialHomeomorph.Composition
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : Set X} {e' : OpenPartialHomeomorph X Y} (hs : IsOpen s) (hs' : IsOpen (↑e '' s)) (hs'' : s ⊆ e.source) : (e.restr s).symm.trans e' ≈ (e.symm.trans e').restr (↑e '' s)
• OpenPartialHomeomorph.lift_openEmbedding_symm 📋 Mathlib.Topology.OpenPartialHomeomorph.Constructions
  {X : Type u_7} {X' : Type u_8} {Z : Type u_9} [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Z] [Nonempty Z] {f : X → X'} (e : OpenPartialHomeomorph X Z) (hf : Topology.IsOpenEmbedding f) : ↑(e.lift_openEmbedding hf).symm = f ∘ ↑e.symm
• OpenPartialHomeomorph.lift_openEmbedding_symm_source 📋 Mathlib.Topology.OpenPartialHomeomorph.Constructions
  {X : Type u_7} {X' : Type u_8} {Z : Type u_9} [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Z] [Nonempty Z] {f : X → X'} (e : OpenPartialHomeomorph X Z) (hf : Topology.IsOpenEmbedding f) : (e.lift_openEmbedding hf).symm.source = e.target
• OpenPartialHomeomorph.lift_openEmbedding_symm_target 📋 Mathlib.Topology.OpenPartialHomeomorph.Constructions
  {X : Type u_7} {X' : Type u_8} {Z : Type u_9} [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Z] [Nonempty Z] {f : X → X'} (e : OpenPartialHomeomorph X Z) (hf : Topology.IsOpenEmbedding f) : (e.lift_openEmbedding hf).symm.target = f '' e.source
• OpenPartialHomeomorph.lift_openEmbedding_trans 📋 Mathlib.Topology.OpenPartialHomeomorph.Constructions
  {X : Type u_7} {X' : Type u_8} {Z : Type u_9} [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Z] [Nonempty Z] {f : X → X'} (e e' : OpenPartialHomeomorph X Z) (hf : Topology.IsOpenEmbedding f) : (e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf) = e.symm.trans e'
• OpenPartialHomeomorph.transHomeomorph_symm_apply 📋 Mathlib.Topology.OpenPartialHomeomorph.Constructions
  {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (f' : Y ≃ₜ Z) : ↑(e.transHomeomorph f').symm = ↑e.symm ∘ ⇑f'.symm
• OpenPartialHomeomorph.prod_symm 📋 Mathlib.Topology.OpenPartialHomeomorph.Constructions
  {X : Type u_1} {X' : Type u_2} {Y : Type u_3} {Y' : Type u_4} [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Y] [TopologicalSpace Y'] (eX : OpenPartialHomeomorph X X') (eY : OpenPartialHomeomorph Y Y') : (eX.prod eY).symm = eX.symm.prod eY.symm
• OpenPartialHomeomorph.lift_openEmbedding_trans_apply 📋 Mathlib.Topology.OpenPartialHomeomorph.Constructions
  {X : Type u_7} {X' : Type u_8} {Z : Type u_9} [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Z] [Nonempty Z] {f : X → X'} (e e' : OpenPartialHomeomorph X Z) (hf : Topology.IsOpenEmbedding f) (z : Z) : ↑((e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf)) z = ↑(e.symm.trans e') z
• OpenPartialHomeomorph.pi_symm_apply 📋 Mathlib.Topology.OpenPartialHomeomorph.Constructions
  {ι : Type u_7} [Finite ι] {X : ι → Type u_8} {Y : ι → Type u_9} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → TopologicalSpace (Y i)] (ei : (i : ι) → OpenPartialHomeomorph (X i) (Y i)) (a✝ : (i : ι) → Y i) (i : ι) : ↑(OpenPartialHomeomorph.pi ei).symm a✝ i = ↑(ei i).symm (a✝ i)
• OpenPartialHomeomorph.prod_symm_apply 📋 Mathlib.Topology.OpenPartialHomeomorph.Constructions
  {X : Type u_1} {X' : Type u_2} {Y : Type u_3} {Y' : Type u_4} [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Y] [TopologicalSpace Y'] (eX : OpenPartialHomeomorph X X') (eY : OpenPartialHomeomorph Y Y') (p : X' × Y') : ↑(eX.prod eY).symm p = (↑eX.symm p.1, ↑eY.symm p.2)
• OpenPartialHomeomorph.prod_symm_trans_prod 📋 Mathlib.Topology.OpenPartialHomeomorph.Constructions
  {X : Type u_1} {X' : Type u_2} {Y : Type u_3} {Y' : Type u_4} [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Y] [TopologicalSpace Y'] (e f : OpenPartialHomeomorph X Y) (e' f' : OpenPartialHomeomorph X' Y') : (e.prod e').symm.trans (f.prod f') = (e.symm.trans f).prod (e'.symm.trans f')
• OpenPartialHomeomorph.subtypeRestr_symm_trans_subtypeRestr 📋 Mathlib.Topology.OpenPartialHomeomorph.Constructions
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {s : TopologicalSpace.Opens X} (hs : Nonempty ↥s) (f f' : OpenPartialHomeomorph X Y) : (f.subtypeRestr hs).symm.trans (f'.subtypeRestr hs) ≈ (f.symm.trans f').restr (f.target ∩ ↑f.symm ⁻¹' ↑s)
• OpenPartialHomeomorph.symm_piecewise 📋 Mathlib.Topology.OpenPartialHomeomorph.Constructions
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e e' : OpenPartialHomeomorph X Y) {s : Set X} {t : Set Y} [(x : X) → Decidable (x ∈ s)] [(y : Y) → Decidable (y ∈ t)] (H : e.IsImage s t) (H' : e'.IsImage s t) (Hs : e.source ∩ frontier s = e'.source ∩ frontier s) (Heq : Set.EqOn (↑e) (↑e') (e.source ∩ frontier s)) : (e.piecewise e' s t H H' Hs Heq).symm = e.symm.piecewise e'.symm t s ⋯ ⋯ ⋯ ⋯
• OpenPartialHomeomorph.subtypeRestr_symm_eqOn 📋 Mathlib.Topology.OpenPartialHomeomorph.Constructions
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {U : TopologicalSpace.Opens X} (hU : Nonempty ↥U) : Set.EqOn (↑e.symm) (Subtype.val ∘ ↑(e.subtypeRestr hU).symm) (e.subtypeRestr hU).target
• OpenPartialHomeomorph.subtypeRestr_symm_apply 📋 Mathlib.Topology.OpenPartialHomeomorph.Constructions
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {U : TopologicalSpace.Opens X} (hU : Nonempty ↥U) {y : Y} (hy : y ∈ (e.subtypeRestr hU).target) : (Subtype.val ∘ ↑(e.subtypeRestr hU).symm) y = ↑e.symm y
• OpenPartialHomeomorph.subtypeRestr_symm_eqOn_of_le 📋 Mathlib.Topology.OpenPartialHomeomorph.Constructions
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {U V : TopologicalSpace.Opens X} (hU : Nonempty ↥U) (hV : Nonempty ↥V) (hUV : U ≤ V) : Set.EqOn (↑(e.subtypeRestr hV).symm) (Set.inclusion hUV ∘ ↑(e.subtypeRestr hU).symm) (e.subtypeRestr hU).target
• Bundle.Trivialization.continuousOn_symm_prodMk_left 📋 Mathlib.Topology.FiberBundle.Trivialization
  {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Bundle.Trivialization F proj) {v : F} : ContinuousOn (fun x => ↑e.symm (x, v)) e.baseSet
• Bundle.Trivialization.proj_symm_apply' 📋 Mathlib.Topology.FiberBundle.Trivialization
  {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Bundle.Trivialization F proj) {b : B} {x : F} (hx : b ∈ e.baseSet) : proj (↑e.symm (b, x)) = b
• Bundle.Trivialization.continuousAt_symm_prodMk_left 📋 Mathlib.Topology.FiberBundle.Trivialization
  {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Bundle.Trivialization F proj) {b : B} {v : F} (hb : b ∈ e.baseSet) : ContinuousAt (fun x => ↑e.symm (x, v)) b
• Bundle.Trivialization.apply_symm_apply' 📋 Mathlib.Topology.FiberBundle.Trivialization
  {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Bundle.Trivialization F proj) {b : B} {x : F} (hx : b ∈ e.baseSet) : ↑e (↑e.symm (b, x)) = (b, x)
• Bundle.Trivialization.symm_coe_proj 📋 Mathlib.Topology.FiberBundle.Trivialization
  {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] {x : B} {y : F} (e : Bundle.Trivialization F Bundle.TotalSpace.proj) (h : x ∈ e.baseSet) : (↑e.symm (x, y)).proj = x
• Bundle.Trivialization.proj_symm_apply 📋 Mathlib.Topology.FiberBundle.Trivialization
  {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Bundle.Trivialization F proj) {x : B × F} (hx : x ∈ e.target) : proj (↑e.symm x) = x.1
• Bundle.Trivialization.symm_apply_mk_proj 📋 Mathlib.Topology.FiberBundle.Trivialization
  {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Bundle.Trivialization F proj) {x : Z} (ex : x ∈ e.source) : ↑e.symm (proj x, (↑e x).2) = x
• Bundle.Trivialization.apply_symm_apply 📋 Mathlib.Topology.FiberBundle.Trivialization
  {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Bundle.Trivialization F proj) {x : B × F} (hx : x ∈ e.target) : ↑e (↑e.symm x) = x
• Bundle.Trivialization.mk_symm 📋 Mathlib.Topology.FiberBundle.Trivialization
  {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] [∀ (x : B), Nonempty (E x)] (e : Bundle.Trivialization F Bundle.TotalSpace.proj) {b : B} (hb : b ∈ e.baseSet) (y : F) : ⟨b, e.symm b y⟩ = ↑e.symm (b, y)
• Bundle.Trivialization.mk_coordChange 📋 Mathlib.Topology.FiberBundle.Trivialization
  {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e₁ e₂ : Bundle.Trivialization F proj) {b : B} (h₁ : b ∈ e₁.baseSet) (h₂ : b ∈ e₂.baseSet) (x : F) : (b, e₁.coordChange e₂ b x) = ↑e₂ (↑e₁.symm (b, x))
• Bundle.Trivialization.map_target 📋 Mathlib.Topology.FiberBundle.Trivialization
  {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Bundle.Trivialization F proj) {x : B × F} (hx : x ∈ e.target) : ↑e.symm x ∈ e.source
• Bundle.Trivialization.symm_apply_apply 📋 Mathlib.Topology.FiberBundle.Trivialization
  {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] (e' : Bundle.Trivialization F Bundle.TotalSpace.proj) {x : Bundle.TotalSpace F E} (hx : x ∈ e'.source) : ↑e'.symm (↑e' x) = x
• Bundle.Trivialization.symm_apply 📋 Mathlib.Topology.FiberBundle.Trivialization
  {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [TopologicalSpace B] [TopologicalSpace F] [TopologicalSpace (Bundle.TotalSpace F E)] [∀ (x : B), Nonempty (E x)] (e : Bundle.Trivialization F Bundle.TotalSpace.proj) {b : B} (hb : b ∈ e.baseSet) (y : F) : e.symm b y = cast ⋯ (↑e.symm (b, y)).snd
• Bundle.Trivialization.domExtend_symm_apply 📋 Mathlib.Topology.FiberBundle.Trivialization
  {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] {s : Set B} (hps : IsOpen (proj ⁻¹' s)) (e : Bundle.Trivialization F fun z => proj ↑z) [Nonempty (Z → F)] (x : B × F) : ↑(Bundle.Trivialization.domExtend hps e).symm x = ↑(↑e.toPretrivialization.symm x)
• Bundle.Trivialization.preimageSingletonHomeomorph_symm_apply 📋 Mathlib.Topology.FiberBundle.Trivialization
  {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Bundle.Trivialization F proj) {b : B} (hb : b ∈ e.baseSet) (p : F) : (e.preimageSingletonHomeomorph hb).symm p = ⟨↑e.symm (b, p), ⋯⟩
• Bundle.Trivialization.preimageHomeomorph_symm_apply 📋 Mathlib.Topology.FiberBundle.Trivialization
  {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Bundle.Trivialization F proj) {s : Set B} (hb : s ⊆ e.baseSet) (p : ↑s × F) : (e.preimageHomeomorph hb).symm p = ⟨↑e.symm (↑p.1, p.2), ⋯⟩
• Bundle.Trivialization.sourceHomeomorphBaseSetProd_symm_apply 📋 Mathlib.Topology.FiberBundle.Trivialization
  {B : Type u_1} {F : Type u_2} {Z : Type u_4} [TopologicalSpace B] [TopologicalSpace F] {proj : Z → B} [TopologicalSpace Z] (e : Bundle.Trivialization F proj) (p : ↑e.baseSet × F) : e.sourceHomeomorphBaseSetProd.symm p = ⟨↑e.symm (↑p.1, p.2), ⋯⟩
• FiberBundleCore.localTriv_symm_apply 📋 Mathlib.Topology.FiberBundle.Basic
  {ι : Type u_1} {B : Type u_2} {F : Type u_3} [TopologicalSpace B] [TopologicalSpace F] (Z : FiberBundleCore ι B F) (i : ι) (p : B × F) : ↑(Z.localTriv i).symm p = ⟨p.1, Z.coordChange i (Z.indexAt p.1) p.1 p.2⟩
• IsLocalHomeomorph.localInverseAt_symm 📋 Mathlib.Topology.IsLocalHomeomorph
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsLocalHomeomorph f) (x : X) : ↑(hf.localInverseAt x).symm = f
• Unitary.openPartialHomeomorph_symm_apply 📋 Mathlib.Analysis.CStarAlgebra.Unitary.Connected
  {A : Type u_1} [CStarAlgebra A] (a : ↥(selfAdjoint A)) : ↑Unitary.openPartialHomeomorph.symm a = selfAdjoint.expUnitary a
• OpenPartialHomeomorph.continuousOn_univBall_symm 📋 Mathlib.Analysis.Normed.Module.Ball.Homeomorph
  {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {P : Type u_2} [PseudoMetricSpace P] [NormedAddTorsor E P] (c : P) (r : ℝ) : ContinuousOn (↑(OpenPartialHomeomorph.univBall c r).symm) (Metric.ball c r)
• OpenPartialHomeomorph.univBall_symm_apply_center 📋 Mathlib.Analysis.Normed.Module.Ball.Homeomorph
  {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {P : Type u_2} [PseudoMetricSpace P] [NormedAddTorsor E P] (c : P) (r : ℝ) : ↑(OpenPartialHomeomorph.univBall c r).symm c = 0
• OpenPartialHomeomorph.univUnitBall_symm_apply_zero 📋 Mathlib.Analysis.Normed.Module.Ball.Homeomorph
  {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] : ↑OpenPartialHomeomorph.univUnitBall.symm 0 = 0
• OpenPartialHomeomorph.univUnitBall_symm_apply 📋 Mathlib.Analysis.Normed.Module.Ball.Homeomorph
  {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (y : E) : ↑OpenPartialHomeomorph.univUnitBall.symm y = (√(1 - ‖y‖ ^ 2))⁻¹ • y
• OpenPartialHomeomorph.unitBallBall_symm_apply 📋 Mathlib.Analysis.Normed.Module.Ball.Homeomorph
  {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {P : Type u_2} [PseudoMetricSpace P] [NormedAddTorsor E P] (c : P) (r : ℝ) (hr : 0 < r) (a : P) : ↑(OpenPartialHomeomorph.unitBallBall c r hr).symm a = r⁻¹ • (a -ᵥ c)
• OpenPartialHomeomorph.contDiffOn_univBall_symm 📋 Mathlib.Analysis.InnerProductSpace.Calculus
  {n : ℕ∞} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {c : E} {r : ℝ} : ContDiffOn ℝ (↑n) (↑(OpenPartialHomeomorph.univBall c r).symm) (Metric.ball c r)
• OpenPartialHomeomorph.contDiff_unitBallBall_symm 📋 Mathlib.Analysis.InnerProductSpace.Calculus
  {n : ℕ∞} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {c : E} {r : ℝ} (hr : 0 < r) : ContDiff ℝ ↑n ↑(OpenPartialHomeomorph.unitBallBall c r hr).symm
• OpenPartialHomeomorph.contDiffOn_univUnitBall_symm 📋 Mathlib.Analysis.InnerProductSpace.Calculus
  {n : ℕ∞} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : ContDiffOn ℝ (↑n) (↑OpenPartialHomeomorph.univUnitBall.symm) (Metric.ball 0 1)
• ImplicitFunctionData.implicitFunction_apply 📋 Mathlib.Analysis.Calculus.Implicit
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] [CompleteSpace G] (φ : ImplicitFunctionData 𝕜 E F G) {x : F} {y : G} : φ.implicitFunction x y = ↑φ.toOpenPartialHomeomorph.symm (x, y)
• ImplicitFunctionData.implicitFunction_def 📋 Mathlib.Analysis.Calculus.Implicit
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] [CompleteSpace G] (φ : ImplicitFunctionData 𝕜 E F G) : φ.implicitFunction = Function.curry ↑(HasStrictFDerivAt.toOpenPartialHomeomorph φ.prodFun ⋯).symm
• StructureGroupoid.symm 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_1} [TopologicalSpace H] (G : StructureGroupoid H) {e : OpenPartialHomeomorph H H} (he : e ∈ G) : e.symm ∈ G
• StructureGroupoid.symm' 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_2} [TopologicalSpace H] (self : StructureGroupoid H) (e : OpenPartialHomeomorph H H) : e ∈ self.members → e.symm ∈ self.members
• mem_groupoid_of_pregroupoid 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_1} [TopologicalSpace H] {PG : Pregroupoid H} {e : OpenPartialHomeomorph H H} : e ∈ PG.groupoid ↔ PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target
• StructureGroupoid.mk 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_2} [TopologicalSpace H] (members : Set (OpenPartialHomeomorph H H)) (trans' : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ∈ members → e.trans e' ∈ members) (symm' : ∀ e ∈ members, e.symm ∈ members) (id_mem' : OpenPartialHomeomorph.refl H ∈ members) (locality' : ∀ (e : OpenPartialHomeomorph H H), (∀ x ∈ e.source, ∃ s, IsOpen s ∧ x ∈ s ∧ e.restr s ∈ members) → e ∈ members) (mem_of_eqOnSource' : ∀ (e e' : OpenPartialHomeomorph H H), e ∈ members → e' ≈ e → e' ∈ members) : StructureGroupoid H
• StructureGroupoid.compatible_of_mem_maximalAtlas_left 📋 Mathlib.Geometry.Manifold.HasGroupoid
  {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} {e' : OpenPartialHomeomorph M H} {x : M} (he' : e' ∈ StructureGroupoid.maximalAtlas M G) : e'.symm.trans (chartAt H x) ∈ G
• StructureGroupoid.compatible_of_mem_maximalAtlas_right 📋 Mathlib.Geometry.Manifold.HasGroupoid
  {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} {e' : OpenPartialHomeomorph M H} {x : M} (he' : e' ∈ StructureGroupoid.maximalAtlas M G) : (chartAt H x).symm.trans e' ∈ G
• StructureGroupoid.compatible_of_mem_maximalAtlas 📋 Mathlib.Geometry.Manifold.HasGroupoid
  {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} {e e' : OpenPartialHomeomorph M H} (he : e ∈ StructureGroupoid.maximalAtlas M G) (he' : e' ∈ StructureGroupoid.maximalAtlas M G) : e.symm.trans e' ∈ G
• HasGroupoid.compatible 📋 Mathlib.Geometry.Manifold.HasGroupoid
  {H : Type u_5} {inst✝ : TopologicalSpace H} {M : Type u_6} {inst✝¹ : TopologicalSpace M} {inst✝² : ChartedSpace H M} {G : StructureGroupoid H} [self : HasGroupoid M G] {e e' : OpenPartialHomeomorph M H} : e ∈ atlas H M → e' ∈ atlas H M → e.symm.trans e' ∈ G
• HasGroupoid.mk 📋 Mathlib.Geometry.Manifold.HasGroupoid
  {H : Type u_5} [TopologicalSpace H] {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} (compatible : ∀ {e e' : OpenPartialHomeomorph M H}, e ∈ atlas H M → e' ∈ atlas H M → e.symm.trans e' ∈ G) : HasGroupoid M G
• StructureGroupoid.compatible 📋 Mathlib.Geometry.Manifold.HasGroupoid
  {H : Type u_5} [TopologicalSpace H] (G : StructureGroupoid H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [HasGroupoid M G] {e e' : OpenPartialHomeomorph M H} (he : e ∈ atlas H M) (he' : e' ∈ atlas H M) : e.symm.trans e' ∈ G
• mem_maximalAtlas_iff 📋 Mathlib.Geometry.Manifold.HasGroupoid
  {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} {e : OpenPartialHomeomorph M H} : e ∈ StructureGroupoid.maximalAtlas M G ↔ ∀ e' ∈ atlas H M, e.symm.trans e' ∈ G ∧ e'.symm.trans e ∈ G
• hasGroupoid_of_pregroupoid 📋 Mathlib.Geometry.Manifold.HasGroupoid
  {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (PG : Pregroupoid H) (h : ∀ {e e' : OpenPartialHomeomorph M H}, e ∈ atlas H M → e' ∈ atlas H M → PG.property (↑(e.symm.trans e')) (e.symm.trans e').source) : HasGroupoid M PG.groupoid
• Structomorph.mk 📋 Mathlib.Geometry.Manifold.HasGroupoid
  {H : Type u} [TopologicalSpace H] {G : StructureGroupoid H} {M : Type u_5} {M' : Type u_6} [TopologicalSpace M] [TopologicalSpace M'] [ChartedSpace H M] [ChartedSpace H M'] (toHomeomorph : M ≃ₜ M') (mem_groupoid : ∀ (c : OpenPartialHomeomorph M H) (c' : OpenPartialHomeomorph M' H), c ∈ atlas H M → c' ∈ atlas H M' → c.symm.trans (toHomeomorph.toOpenPartialHomeomorph.trans c') ∈ G) : Structomorph G M M'
• Structomorph.mem_groupoid 📋 Mathlib.Geometry.Manifold.HasGroupoid
  {H : Type u} [TopologicalSpace H] {G : StructureGroupoid H} {M : Type u_5} {M' : Type u_6} [TopologicalSpace M] [TopologicalSpace M'] [ChartedSpace H M] [ChartedSpace H M'] (self : Structomorph G M M') (c : OpenPartialHomeomorph M H) (c' : OpenPartialHomeomorph M' H) : c ∈ atlas H M → c' ∈ atlas H M' → c.symm.trans (self.toOpenPartialHomeomorph.trans c') ∈ G
• StructureGroupoid.trans_restricted 📋 Mathlib.Geometry.Manifold.HasGroupoid
  {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {e e' : OpenPartialHomeomorph M H} {G : StructureGroupoid H} (he : e ∈ atlas H M) (he' : e' ∈ atlas H M) [HasGroupoid M G] [ClosedUnderRestriction G] {s : TopologicalSpace.Opens M} (hs : Nonempty ↥s) : (e.subtypeRestr hs).symm.trans (e'.subtypeRestr hs) ∈ G
• TopologicalSpace.Opens.chartAt_subtype_val_symm_eventuallyEq 📋 Mathlib.Geometry.Manifold.HasGroupoid
  {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (U : TopologicalSpace.Opens M) {x : ↥U} : ↑(chartAt H ↑x).symm =ᶠ[nhds (↑(chartAt H ↑x) ↑x)] Subtype.val ∘ ↑(chartAt H x).symm
• TopologicalSpace.Opens.chartAt_inclusion_symm_eventuallyEq 📋 Mathlib.Geometry.Manifold.HasGroupoid
  {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {U V : TopologicalSpace.Opens M} (hUV : U ≤ V) {x : ↥U} : ↑(chartAt H (TopologicalSpace.Opens.inclusion hUV x)).symm =ᶠ[nhds (↑(chartAt H (TopologicalSpace.Opens.inclusion hUV x)) (Set.inclusion hUV x))] TopologicalSpace.Opens.inclusion hUV ∘ ↑(chartAt H x).symm
• symm_trans_mem_contDiffGroupoid 📋 Mathlib.Geometry.Manifold.IsManifold.Basic
  {n : WithTop ℕ∞} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] (e : OpenPartialHomeomorph M H) : e.symm.trans e ∈ contDiffGroupoid n I
• IsManifold.compatible_of_mem_maximalAtlas 📋 Mathlib.Geometry.Manifold.IsManifold.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {e e' : OpenPartialHomeomorph M H} (he : e ∈ IsManifold.maximalAtlas I n M) (he' : e' ∈ IsManifold.maximalAtlas I n M) : e.symm.trans e' ∈ contDiffGroupoid n I
• isManifold_of_contDiffOn 📋 Mathlib.Geometry.Manifold.IsManifold.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (M : Type u_4) [TopologicalSpace M] [ChartedSpace H M] (h : ∀ (e e' : OpenPartialHomeomorph M H), e ∈ atlas H M → e' ∈ atlas H M → ContDiffOn 𝕜 n (↑I ∘ ↑(e.symm.trans e') ∘ ↑I.symm) (↑I.symm ⁻¹' (e.symm.trans e').source ∩ Set.range ↑I)) : IsManifold I n M
• OpenPartialHomeomorph.extend_coe_symm 📋 Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
  {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} : ↑(f.extend I).symm = ↑f.symm ∘ ↑I.symm
• extChartAt_coe_symm 📋 Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
  {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] (x : M) : ↑(extChartAt I x).symm = ↑(chartAt H x).symm ∘ ↑I.symm
• ModelWithCorners.extendCoordChange_source 📋 Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
  {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} {e e' : OpenPartialHomeomorph M H} : (ModelWithCorners.extendCoordChange e e').source = ↑I '' (e.symm.trans e').source
• ModelWithCorners.extendCoordChange_target 📋 Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
  {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} {e e' : OpenPartialHomeomorph M H} : (ModelWithCorners.extendCoordChange e e').target = ↑I '' (e.symm.trans e').target
• writtenInExtChartAt_chartAt_symm 📋 Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
  {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] {x : M} {y : E} (h : y ∈ (extChartAt I x).target) : writtenInExtChartAt I I (↑(chartAt H x) x) (↑(chartAt H x).symm) y = y
• ext_coord_change_source 📋 Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
  {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] {I : ModelWithCorners 𝕜 E H} [ChartedSpace H M] (x x' : M) : ((extChartAt I x').symm.trans (extChartAt I x)).source = ↑I '' ((chartAt H x').symm.trans (chartAt H x)).source
• writtenInExtChartAt_chartAt_symm_comp 📋 Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
  {𝕜 : Type u_1} {E : Type u_2} {H : Type u_4} {M' : Type u_6} {H' : Type u_7} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] [ChartedSpace H H'] (x : M') {y : E} (hy : y ∈ (extChartAt I x).target) : writtenInExtChartAt I I (↑(chartAt H' x) x) (↑(chartAt H' x).symm) y = y
• OpenPartialHomeomorph.extend_symm_continuousWithinAt_comp_right_iff 📋 Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
  {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {X : Type u_8} [TopologicalSpace X] {g : M → X} {s : Set M} {x : M} : ContinuousWithinAt (g ∘ ↑(f.extend I).symm) (↑(f.extend I).symm ⁻¹' s ∩ Set.range ↑I) (↑(f.extend I) x) ↔ ContinuousWithinAt (g ∘ ↑f.symm) (↑f.symm ⁻¹' s) (↑f x)
• StructureGroupoid.LocalInvariantProp.liftPropAt_chart_symm 📋 Mathlib.Geometry.Manifold.LocalInvariantProperties
  {H : Type u_1} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} {x : M} {Q : (H → H) → Set H → H → Prop} [HasGroupoid M G] (hG : G.LocalInvariantProp G Q) (hQ : ∀ (y : H), Q id Set.univ y) : ChartedSpace.LiftPropAt Q (↑(chartAt H x).symm) (↑(chartAt H x) x)
• StructureGroupoid.LocalInvariantProp.liftPropOn_chart_symm 📋 Mathlib.Geometry.Manifold.LocalInvariantProperties
  {H : Type u_1} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} {x : M} {Q : (H → H) → Set H → H → Prop} [HasGroupoid M G] (hG : G.LocalInvariantProp G Q) (hQ : ∀ (y : H), Q id Set.univ y) : ChartedSpace.LiftPropOn Q (↑(chartAt H x).symm) (chartAt H x).target
• StructureGroupoid.LocalInvariantProp.liftPropOn_symm_of_mem_maximalAtlas 📋 Mathlib.Geometry.Manifold.LocalInvariantProperties
  {H : Type u_1} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} {e : OpenPartialHomeomorph M H} {Q : (H → H) → Set H → H → Prop} (hG : G.LocalInvariantProp G Q) (hQ : ∀ (y : H), Q id Set.univ y) (he : e ∈ StructureGroupoid.maximalAtlas M G) : ChartedSpace.LiftPropOn Q (↑e.symm) e.target
• ChartedSpace.liftProp_iff 📋 Mathlib.Geometry.Manifold.LocalInvariantProperties
  {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {P : (H → H') → Set H → H → Prop} {f : M → M'} : ChartedSpace.LiftProp P f ↔ Continuous f ∧ ∀ (x : M), P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) Set.univ (↑(chartAt H x) x)
• ChartedSpace.liftPropAt_iff 📋 Mathlib.Geometry.Manifold.LocalInvariantProperties
  {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {P : (H → H') → Set H → H → Prop} {f : M → M'} {x : M} : ChartedSpace.LiftPropAt P f x ↔ ContinuousAt f x ∧ P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) Set.univ (↑(chartAt H x) x)
• StructureGroupoid.liftPropWithinAt_self_target 📋 Mathlib.Geometry.Manifold.LocalInvariantProperties
  {H : Type u_1} {M : Type u_2} {H' : Type u_3} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] {P : (H → H') → Set H → H → Prop} {s : Set M} {x : M} {f : M → H'} : ChartedSpace.LiftPropWithinAt P f s x ↔ ContinuousWithinAt f s x ∧ P (f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)
• StructureGroupoid.LocalInvariantProp.liftPropAt_symm_of_mem_maximalAtlas 📋 Mathlib.Geometry.Manifold.LocalInvariantProperties
  {H : Type u_1} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} {e : OpenPartialHomeomorph M H} {Q : (H → H) → Set H → H → Prop} {x : H} (hG : G.LocalInvariantProp G Q) (hQ : ∀ (y : H), Q id Set.univ y) (he : e ∈ StructureGroupoid.maximalAtlas M G) (hx : x ∈ e.target) : ChartedSpace.LiftPropAt Q (↑e.symm) x
• StructureGroupoid.LocalInvariantProp.right_invariance' 📋 Mathlib.Geometry.Manifold.LocalInvariantProperties
  {H : Type u_1} {H' : Type u_3} [TopologicalSpace H] [TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} (self : G.LocalInvariantProp G' P) {s : Set H} {x : H} {f : H → H'} {e : OpenPartialHomeomorph H H} : e ∈ G → x ∈ e.source → P f s x → P (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
• StructureGroupoid.LocalInvariantProp.right_invariance 📋 Mathlib.Geometry.Manifold.LocalInvariantProperties
  {H : Type u_1} {H' : Type u_3} [TopologicalSpace H] [TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} (hG : G.LocalInvariantProp G' P) {s : Set H} {x : H} {f : H → H'} {e : OpenPartialHomeomorph H H} (he : e ∈ G) (hxe : x ∈ e.source) : P (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔ P f s x
• ChartedSpace.LiftPropWithinAt.prop 📋 Mathlib.Geometry.Manifold.LocalInvariantProperties
  {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {P : (H → H') → Set H → H → Prop} {f : M → M'} {s : Set M} {x : M} (self : ChartedSpace.LiftPropWithinAt P f s x) : P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)
• ChartedSpace.LiftPropWithinAt.mk 📋 Mathlib.Geometry.Manifold.LocalInvariantProperties
  {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {P : (H → H') → Set H → H → Prop} {f : M → M'} {s : Set M} {x : M} (continuousWithinAt : ContinuousWithinAt f s x) (prop : P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)) : ChartedSpace.LiftPropWithinAt P f s x
• ChartedSpace.liftPropWithinAt_iff' 📋 Mathlib.Geometry.Manifold.LocalInvariantProperties
  {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] (P : (H → H') → Set H → H → Prop) (f : M → M') (s : Set M) (x : M) : ChartedSpace.LiftPropWithinAt P f s x ↔ ContinuousWithinAt f s x ∧ P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)
• StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_source 📋 Mathlib.Geometry.Manifold.LocalInvariantProperties
  {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {e : OpenPartialHomeomorph M H} {P : (H → H') → Set H → H → Prop} {g : M → M'} {s : Set M} {x : M} (hG : G.LocalInvariantProp G' P) (he : e ∈ StructureGroupoid.maximalAtlas M G) (xe : x ∈ e.source) : ChartedSpace.LiftPropWithinAt P g s x ↔ ChartedSpace.LiftPropWithinAt P (g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
• StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_source_aux 📋 Mathlib.Geometry.Manifold.LocalInvariantProperties
  {H : Type u_1} {M : Type u_2} {H' : Type u_3} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {e : OpenPartialHomeomorph M H} {P : (H → H') → Set H → H → Prop} {s : Set M} {x : M} (hG : G.LocalInvariantProp G' P) (g : M → H') (he : e ∈ StructureGroupoid.maximalAtlas M G) (xe : x ∈ e.source) : P (g ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x) ↔ P (g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
• StructureGroupoid.LocalInvariantProp.liftPropWithinAt_iff 📋 Mathlib.Geometry.Manifold.LocalInvariantProperties
  {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} {s : Set M} {x : M} (hG : G.LocalInvariantProp G' P) {f : M → M'} : ChartedSpace.LiftPropWithinAt P f s x ↔ ContinuousWithinAt f s x ∧ P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) ((chartAt H x).target ∩ ↑(chartAt H x).symm ⁻¹' (s ∩ f ⁻¹' (chartAt H' (f x)).source)) (↑(chartAt H x) x)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59