Loogle!

Result

Found 156 declarations mentioning StructureGroupoid.

• StructureGroupoid 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  (H : Type u_2) [TopologicalSpace H] : Type u_2
• continuousGroupoid 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  (H : Type u_2) [TopologicalSpace H] : StructureGroupoid H
• idGroupoid 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  (H : Type u_2) [TopologicalSpace H] : StructureGroupoid H
• idRestrGroupoid 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_1} [TopologicalSpace H] : StructureGroupoid H
• ClosedUnderRestriction 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_1} [TopologicalSpace H] (G : StructureGroupoid H) : Prop
• instCompleteLatticeStructureGroupoid 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_1} [TopologicalSpace H] : CompleteLattice (StructureGroupoid H)
• instInfSetStructureGroupoid 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_1} [TopologicalSpace H] : InfSet (StructureGroupoid H)
• instInhabitedStructureGroupoid 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_1} [TopologicalSpace H] : Inhabited (StructureGroupoid H)
• instMinStructureGroupoid 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_1} [TopologicalSpace H] : Min (StructureGroupoid H)
• StructureGroupoid.partialOrder 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_1} [TopologicalSpace H] : PartialOrder (StructureGroupoid H)
• Pregroupoid.groupoid 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_1} [TopologicalSpace H] (PG : Pregroupoid H) : StructureGroupoid H
• instMembershipOpenPartialHomeomorphStructureGroupoid 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_1} [TopologicalSpace H] : Membership (OpenPartialHomeomorph H H) (StructureGroupoid H)
• instSetLikeStructureGroupoidOpenPartialHomeomorph 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  (H : Type u_2) [TopologicalSpace H] : SetLike (StructureGroupoid H) (OpenPartialHomeomorph H H)
• StructureGroupoid.members 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_2} [TopologicalSpace H] (self : StructureGroupoid H) : Set (OpenPartialHomeomorph H H)
• instStructureGroupoidOrderBot 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_1} [TopologicalSpace H] : OrderBot (StructureGroupoid H)
• instStructureGroupoidOrderTop 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_1} [TopologicalSpace H] : OrderTop (StructureGroupoid H)
• StructureGroupoid.id_mem 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_1} [TopologicalSpace H] (G : StructureGroupoid H) : OpenPartialHomeomorph.refl H ∈ G
• idRestrGroupoid_mem 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_1} [TopologicalSpace H] {s : Set H} (hs : IsOpen s) : OpenPartialHomeomorph.ofSet s hs ∈ idRestrGroupoid
• closedUnderRestriction_iff_id_le 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_1} [TopologicalSpace H] (G : StructureGroupoid H) : ClosedUnderRestriction G ↔ idRestrGroupoid ≤ G
• StructureGroupoid.id_mem' 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_2} [TopologicalSpace H] (self : StructureGroupoid H) : OpenPartialHomeomorph.refl H ∈ self.members
• 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
• groupoid_of_pregroupoid_le 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_1} [TopologicalSpace H] (PG₁ PG₂ : Pregroupoid H) (h : ∀ (f : H → H) (s : Set H), PG₁.property f s → PG₂.property f s) : PG₁.groupoid ≤ PG₂.groupoid
• closedUnderRestriction' 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_1} [TopologicalSpace H] {G : StructureGroupoid H} [ClosedUnderRestriction G] {e : OpenPartialHomeomorph H H} (he : e ∈ G) {s : Set H} (hs : IsOpen s) : e.restr s ∈ G
• ClosedUnderRestriction.closedUnderRestriction 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_1} {inst✝ : TopologicalSpace H} {G : StructureGroupoid H} [self : ClosedUnderRestriction G] {e : OpenPartialHomeomorph H H} : e ∈ G → ∀ (s : Set H), IsOpen s → e.restr s ∈ G
• ClosedUnderRestriction.mk 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_1} [TopologicalSpace H] {G : StructureGroupoid H} (closedUnderRestriction : ∀ {e : OpenPartialHomeomorph H H}, e ∈ G → ∀ (s : Set H), IsOpen s → e.restr s ∈ G) : ClosedUnderRestriction G
• StructureGroupoid.le_iff 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_1} [TopologicalSpace H] {G₁ G₂ : StructureGroupoid H} : G₁ ≤ G₂ ↔ ∀ e ∈ G₁, e ∈ 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
• StructureGroupoid.mem_of_eqOnSource 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_1} [TopologicalSpace H] (G : StructureGroupoid H) {e e' : OpenPartialHomeomorph H H} (he : e ∈ G) (h : e' ≈ e) : e' ∈ G
• StructureGroupoid.mem_iff_of_eqOnSource 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_1} [TopologicalSpace H] {G : StructureGroupoid H} {e e' : OpenPartialHomeomorph H H} (h : e ≈ e') : e ∈ G ↔ e' ∈ G
• StructureGroupoid.trans 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_1} [TopologicalSpace H] (G : StructureGroupoid H) {e e' : OpenPartialHomeomorph H H} (he : e ∈ G) (he' : e' ∈ G) : e.trans e' ∈ G
• StructureGroupoid.mem_of_eqOnSource' 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_2} [TopologicalSpace H] (self : StructureGroupoid H) (e e' : OpenPartialHomeomorph H H) : e ∈ self.members → e' ≈ e → e' ∈ 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.locality 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_1} [TopologicalSpace H] (G : StructureGroupoid H) {e : OpenPartialHomeomorph H H} (h : ∀ x ∈ e.source, ∃ s, IsOpen s ∧ x ∈ s ∧ e.restr s ∈ G) : e ∈ G
• StructureGroupoid.trans' 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_2} [TopologicalSpace H] (self : StructureGroupoid H) (e e' : OpenPartialHomeomorph H H) : e ∈ self.members → e' ∈ self.members → e.trans e' ∈ self.members
• StructureGroupoid.locality' 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_2} [TopologicalSpace H] (self : StructureGroupoid H) (e : OpenPartialHomeomorph H H) : (∀ x ∈ e.source, ∃ s, IsOpen s ∧ x ∈ s ∧ e.restr s ∈ self.members) → e ∈ self.members
• StructureGroupoid.restr_mem_of_eqOn 📋 Mathlib.Geometry.Manifold.StructureGroupoid
  {H : Type u_1} [TopologicalSpace H] {G : StructureGroupoid H} [ClosedUnderRestriction G] {e e' : OpenPartialHomeomorph H H} (he : e ∈ G) {s : Set H} (hs : IsOpen s) (heq : Set.EqOn (↑e) (↑e') s) (hsub : e'.source ∩ s ⊆ e.source) : e'.restr s ∈ G
• 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
• HasGroupoid 📋 Mathlib.Geometry.Manifold.HasGroupoid
  {H : Type u_5} [TopologicalSpace H] (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] (G : StructureGroupoid H) : Prop
• hasGroupoid_model_space 📋 Mathlib.Geometry.Manifold.HasGroupoid
  (H : Type u_5) [TopologicalSpace H] (G : StructureGroupoid H) : HasGroupoid H G
• StructureGroupoid.maximalAtlas 📋 Mathlib.Geometry.Manifold.HasGroupoid
  {H : Type u} (M : Type u_2) [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (G : StructureGroupoid H) : Set (OpenPartialHomeomorph M H)
• Structomorph 📋 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'] : Type (max u_5 u_6)
• Structomorph.refl 📋 Mathlib.Geometry.Manifold.HasGroupoid
  {H : Type u} [TopologicalSpace H] {G : StructureGroupoid H} (M : Type u_5) [TopologicalSpace M] [ChartedSpace H M] [HasGroupoid M G] : Structomorph G M M
• StructureGroupoid.id_mem_maximalAtlas 📋 Mathlib.Geometry.Manifold.HasGroupoid
  {H : Type u} [TopologicalSpace H] (G : StructureGroupoid H) : OpenPartialHomeomorph.refl H ∈ StructureGroupoid.maximalAtlas H G
• Structomorph.toHomeomorph 📋 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') : M ≃ₜ M'
• Topology.IsOpenEmbedding.singleton_hasGroupoid 📋 Mathlib.Geometry.Manifold.HasGroupoid
  {H : Type u} [TopologicalSpace H] {α : Type u_5} [TopologicalSpace α] [Nonempty α] {f : α → H} (h : Topology.IsOpenEmbedding f) (G : StructureGroupoid H) [ClosedUnderRestriction G] : HasGroupoid α G
• Structomorph.symm 📋 Mathlib.Geometry.Manifold.HasGroupoid
  {H : Type u} {M : Type u_2} {M' : Type u_3} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace M'] {G : StructureGroupoid H} [ChartedSpace H M'] (e : Structomorph G M M') : Structomorph G M' M
• StructureGroupoid.subset_maximalAtlas 📋 Mathlib.Geometry.Manifold.HasGroupoid
  {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (G : StructureGroupoid H) [HasGroupoid M G] : atlas H M ⊆ StructureGroupoid.maximalAtlas M G
• hasGroupoid_inf_iff 📋 Mathlib.Geometry.Manifold.HasGroupoid
  {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G₁ G₂ : StructureGroupoid H} : HasGroupoid M (G₁ ⊓ G₂) ↔ HasGroupoid M G₁ ∧ HasGroupoid M G₂
• hasGroupoid_of_le 📋 Mathlib.Geometry.Manifold.HasGroupoid
  {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G₁ G₂ : StructureGroupoid H} (h : HasGroupoid M G₁) (hle : G₁ ≤ G₂) : HasGroupoid M G₂
• OpenPartialHomeomorph.singleton_hasGroupoid 📋 Mathlib.Geometry.Manifold.HasGroupoid
  {H : Type u} [TopologicalSpace H] {α : Type u_5} [TopologicalSpace α] (e : OpenPartialHomeomorph α H) (h : e.source = Set.univ) (G : StructureGroupoid H) [ClosedUnderRestriction G] : HasGroupoid α G
• StructureGroupoid.mem_maximalAtlas_of_mem_groupoid 📋 Mathlib.Geometry.Manifold.HasGroupoid
  {H : Type u} [TopologicalSpace H] (G : StructureGroupoid H) {f : OpenPartialHomeomorph H H} (hf : f ∈ G) : f ∈ StructureGroupoid.maximalAtlas H G
• StructureGroupoid.chart_mem_maximalAtlas 📋 Mathlib.Geometry.Manifold.HasGroupoid
  {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (G : StructureGroupoid H) [HasGroupoid M G] (x : M) : chartAt H x ∈ StructureGroupoid.maximalAtlas M G
• Structomorph.trans 📋 Mathlib.Geometry.Manifold.HasGroupoid
  {H : Type u} {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace M'] [TopologicalSpace M''] {G : StructureGroupoid H} [ChartedSpace H M'] [ChartedSpace H M''] (e : Structomorph G M M') (e' : Structomorph G M' M'') : Structomorph G M M''
• StructureGroupoid.maximalAtlas_mono 📋 Mathlib.Geometry.Manifold.HasGroupoid
  {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G G' : StructureGroupoid H} (h : G ≤ G') : StructureGroupoid.maximalAtlas M G ⊆ StructureGroupoid.maximalAtlas M G'
• TopologicalSpace.Opens.instHasGroupoid 📋 Mathlib.Geometry.Manifold.HasGroupoid
  {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (G : StructureGroupoid H) [HasGroupoid M G] (s : TopologicalSpace.Opens M) [ClosedUnderRestriction G] : HasGroupoid (↥s) G
• 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
• restr_mem_maximalAtlas 📋 Mathlib.Geometry.Manifold.HasGroupoid
  {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (G : StructureGroupoid H) [ClosedUnderRestriction G] {e : OpenPartialHomeomorph M H} (he : e ∈ StructureGroupoid.maximalAtlas M G) {s : Set M} (hs : IsOpen s) : e.restr s ∈ StructureGroupoid.maximalAtlas M G
• StructureGroupoid.mem_maximalAtlas_of_eqOnSource 📋 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} (h : e' ≈ e) (he : e ∈ StructureGroupoid.maximalAtlas M G) : e' ∈ StructureGroupoid.maximalAtlas M 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
• 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
• OpenPartialHomeomorph.toStructomorph 📋 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} (he : e ∈ atlas H M) [HasGroupoid M G] [ClosedUnderRestriction G] : have s := { carrier := e.source, is_open' := ⋯ }; have t := { carrier := e.target, is_open' := ⋯ }; Structomorph G ↥s ↥t
• 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
• StructureGroupoid.subtypeRestr_mem_maximalAtlas 📋 Mathlib.Geometry.Manifold.HasGroupoid
  {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {e : OpenPartialHomeomorph M H} (he : e ∈ atlas H M) {s : TopologicalSpace.Opens M} (hs : Nonempty ↥s) {G : StructureGroupoid H} [HasGroupoid M G] [ClosedUnderRestriction G] : e.subtypeRestr hs ∈ StructureGroupoid.maximalAtlas (↥s) G
• StructureGroupoid.restriction_mem_maximalAtlas_subtype 📋 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} (he : e ∈ atlas H M) (hs : Nonempty ↑e.source) [HasGroupoid M G] [ClosedUnderRestriction G] : let s := { carrier := e.source, is_open' := ⋯ }; let t := { carrier := e.target, is_open' := ⋯ }; ∀ c' ∈ atlas H ↥t, e.toHomeomorphSourceTarget.toOpenPartialHomeomorph.trans c' ∈ StructureGroupoid.maximalAtlas (↥s) G
• 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) : StructureGroupoid H
• contDiffGroupoid_zero_eq 📋 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} : contDiffGroupoid 0 I = continuousGroupoid H
• ofSet_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} {s : Set H} (hs : IsOpen s) : OpenPartialHomeomorph.ofSet s hs ∈ contDiffGroupoid n I
• ContinuousGroupoid.mem_of_source_eq_empty 📋 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} (f : OpenPartialHomeomorph H H) (hf : f.source = ∅) : f ∈ continuousGroupoid H
• 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
• contDiffGroupoid_le 📋 Mathlib.Geometry.Manifold.IsManifold.Basic
  {m n : WithTop ℕ∞} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} (h : m ≤ n) : contDiffGroupoid n I ≤ contDiffGroupoid m I
• ContDiffGroupoid.mem_of_source_eq_empty 📋 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} (f : OpenPartialHomeomorph H H) (hf : f.source = ∅) : f ∈ 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
• contDiffGroupoid_prod 📋 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] {E' : Type u_5} {H' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {e : OpenPartialHomeomorph H H} {e' : OpenPartialHomeomorph H' H'} (he : e ∈ contDiffGroupoid n I) (he' : e' ∈ contDiffGroupoid n I') : e.prod e' ∈ contDiffGroupoid n (I.prod I')
• StructureGroupoid.IsLocalStructomorphWithinAt 📋 Mathlib.Geometry.Manifold.LocalInvariantProperties
  {H : Type u_1} [TopologicalSpace H] (G : StructureGroupoid H) (f : H → H) (s : Set H) (x : H) : Prop
• StructureGroupoid.LocalInvariantProp 📋 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) : Prop
• StructureGroupoid.isLocalStructomorphWithinAt_localInvariantProp 📋 Mathlib.Geometry.Manifold.LocalInvariantProperties
  {H : Type u_1} [TopologicalSpace H] (G : StructureGroupoid H) [ClosedUnderRestriction G] : G.LocalInvariantProp G G.IsLocalStructomorphWithinAt
• StructureGroupoid.LocalInvariantProp.liftProp_id 📋 Mathlib.Geometry.Manifold.LocalInvariantProperties
  {H : Type u_1} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} {Q : (H → H) → Set H → H → Prop} (hG : G.LocalInvariantProp G Q) (hQ : ∀ (y : H), Q id Set.univ y) : ChartedSpace.LiftProp Q id
• StructureGroupoid.LocalInvariantProp.congr 📋 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 g : H → H'} (h : f =ᶠ[nhds x] g) (hP : P f s x) : P g s x
• StructureGroupoid.LocalInvariantProp.congr' 📋 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 g : H → H'} (h : f =ᶠ[nhds x] g) (hP : P g s x) : P f s x
• StructureGroupoid.LocalInvariantProp.congr_set 📋 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 t : Set H} {x : H} {f : H → H'} (hu : s =ᶠ[nhds x] t) : P f s x ↔ P f t x
• StructureGroupoid.LocalInvariantProp.congr_iff 📋 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 g : H → H'} (h : f =ᶠ[nhds x] g) : P f s x ↔ P g s x
• StructureGroupoid.LocalInvariantProp.congr_nhdsWithin 📋 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 g : H → H'} (h1 : f =ᶠ[nhdsWithin x s] g) (h2 : f x = g x) (hP : P f s x) : P g s x
• StructureGroupoid.LocalInvariantProp.congr_nhdsWithin' 📋 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 g : H → H'} (h1 : f =ᶠ[nhdsWithin x s] g) (h2 : f x = g x) (hP : P g s x) : P f s x
• StructureGroupoid.LocalInvariantProp.congr_iff_nhdsWithin 📋 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 g : H → H'} (h1 : f =ᶠ[nhdsWithin x s] g) (h2 : f x = g x) : P f s x ↔ P g s x
• StructureGroupoid.LocalInvariantProp.is_local 📋 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} {u : Set H} {f : H → H'} : IsOpen u → x ∈ u → (P f s x ↔ P f (s ∩ u) x)
• StructureGroupoid.LocalInvariantProp.congr_set_fun 📋 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 t : Set H} {x : H} {f g : H → H'} (hu : s =ᶠ[nhds x] t) (h : f =ᶠ[nhds x] g) : P f s x ↔ P g t x
• StructureGroupoid.LocalInvariantProp.is_local_nhds 📋 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 u : Set H} {x : H} {f : H → H'} (hu : u ∈ nhdsWithin x s) : P f s x ↔ P f (s ∩ u) x
• StructureGroupoid.LocalInvariantProp.congr_of_forall 📋 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 g : H → H'} : (∀ y ∈ s, f y = g y) → f x = g x → P f s x → P g s x
• StructureGroupoid.LocalInvariantProp.liftPropAt_chart 📋 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)) x
• StructureGroupoid.LocalInvariantProp.liftPropOn_of_mem_groupoid 📋 Mathlib.Geometry.Manifold.LocalInvariantProperties
  {H : Type u_1} [TopologicalSpace H] {G : StructureGroupoid H} {Q : (H → H) → Set H → H → Prop} (hG : G.LocalInvariantProp G Q) (hQ : ∀ (y : H), Q id Set.univ y) {f : OpenPartialHomeomorph H H} (hf : f ∈ G) : ChartedSpace.LiftPropOn Q (↑f) f.source
• StructureGroupoid.LocalInvariantProp.liftPropAt_congr_of_eventuallyEq 📋 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} {g g' : M → M'} {x : M} (hG : G.LocalInvariantProp G' P) (h : ChartedSpace.LiftPropAt P g x) (h₁ : g' =ᶠ[nhds x] g) : ChartedSpace.LiftPropAt P g' x
• StructureGroupoid.LocalInvariantProp.liftPropAt_congr_iff_of_eventuallyEq 📋 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} {g g' : M → M'} {x : M} (hG : G.LocalInvariantProp G' P) (h₁ : g' =ᶠ[nhds x] g) : ChartedSpace.LiftPropAt P g' x ↔ ChartedSpace.LiftPropAt P g 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.liftPropAt_of_liftPropWithinAt 📋 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} {g : M → M'} {s : Set M} {x : M} (hG : G.LocalInvariantProp G' P) (h : ChartedSpace.LiftPropWithinAt P g s x) (hs : s ∈ nhds x) : ChartedSpace.LiftPropAt P g x
• StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_set 📋 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} {g : M → M'} {s t : Set M} {x : M} (hG : G.LocalInvariantProp G' P) (hu : s =ᶠ[nhds x] t) : ChartedSpace.LiftPropWithinAt P g s x ↔ ChartedSpace.LiftPropWithinAt P g t x
• StructureGroupoid.LocalInvariantProp.liftPropWithinAt_of_liftPropAt_of_mem_nhds 📋 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} {g : M → M'} {s : Set M} {x : M} (hG : G.LocalInvariantProp G' P) (h : ChartedSpace.LiftPropAt P g x) (hs : s ∈ nhds x) : ChartedSpace.LiftPropWithinAt P g s x
• StructureGroupoid.LocalInvariantProp.liftPropOn_chart 📋 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)) (chartAt H x).source
• StructureGroupoid.LocalInvariantProp.liftPropAt_of_mem_groupoid 📋 Mathlib.Geometry.Manifold.LocalInvariantProperties
  {H : Type u_1} [TopologicalSpace H] {G : StructureGroupoid H} {Q : (H → H) → Set H → H → Prop} (hG : G.LocalInvariantProp G Q) (hQ : ∀ (y : H), Q id Set.univ y) {f : OpenPartialHomeomorph H H} (hf : f ∈ G) {x : H} (hx : x ∈ f.source) : ChartedSpace.LiftPropAt Q (↑f) x
• StructureGroupoid.LocalInvariantProp.liftPropOn_congr 📋 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} {g g' : M → M'} {s : Set M} (hG : G.LocalInvariantProp G' P) (h : ChartedSpace.LiftPropOn P g s) (h₁ : ∀ y ∈ s, g' y = g y) : ChartedSpace.LiftPropOn P g' s
• StructureGroupoid.LocalInvariantProp.liftProp_of_locally_liftPropOn 📋 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} {g : M → M'} (hG : G.LocalInvariantProp G' P) (h : ∀ (x : M), ∃ u, IsOpen u ∧ x ∈ u ∧ ChartedSpace.LiftPropOn P g u) : ChartedSpace.LiftProp P g
• StructureGroupoid.LocalInvariantProp.liftPropOn_congr_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} {g g' : M → M'} {s : Set M} (hG : G.LocalInvariantProp G' P) (h₁ : ∀ y ∈ s, g' y = g y) : ChartedSpace.LiftPropOn P g' s ↔ ChartedSpace.LiftPropOn P g s
• 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.liftPropWithinAt_congr_of_eventuallyEq 📋 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} {g g' : M → M'} {s : Set M} {x : M} (hG : G.LocalInvariantProp G' P) (h : ChartedSpace.LiftPropWithinAt P g s x) (h₁ : g' =ᶠ[nhdsWithin x s] g) (hx : g' x = g x) : ChartedSpace.LiftPropWithinAt P g' s x
• StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_iff_of_eventuallyEq 📋 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} {g g' : M → M'} {s : Set M} {x : M} (hG : G.LocalInvariantProp G' P) (h₁ : g' =ᶠ[nhdsWithin x s] g) (hx : g' x = g x) : ChartedSpace.LiftPropWithinAt P g' s x ↔ ChartedSpace.LiftPropWithinAt P g s x
• StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_of_eventuallyEq_of_mem 📋 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} {g g' : M → M'} {s : Set M} {x : M} (hG : G.LocalInvariantProp G' P) (h : ChartedSpace.LiftPropWithinAt P g s x) (h₁ : g' =ᶠ[nhdsWithin x s] g) (h₂ : x ∈ s) : ChartedSpace.LiftPropWithinAt P g' s x
• StructureGroupoid.LocalInvariantProp.liftPropWithinAt_inter 📋 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} {g : M → M'} {s t : Set M} {x : M} (hG : G.LocalInvariantProp G' P) (ht : t ∈ nhds x) : ChartedSpace.LiftPropWithinAt P g (s ∩ t) x ↔ ChartedSpace.LiftPropWithinAt P g s x
• StructureGroupoid.LocalInvariantProp.left_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') (hfs : ContinuousWithinAt f s x) (hxe' : f x ∈ e'.source) : P (↑e' ∘ f) s x ↔ P f s x
• StructureGroupoid.LocalInvariantProp.liftPropWithinAt_inter' 📋 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} {g : M → M'} {s t : Set M} {x : M} (hG : G.LocalInvariantProp G' P) (ht : t ∈ nhdsWithin x s) : ChartedSpace.LiftPropWithinAt P g (s ∩ t) x ↔ ChartedSpace.LiftPropWithinAt P g s x
• StructureGroupoid.LocalInvariantProp.liftPropOn_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) e.source
• StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr 📋 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} {g g' : M → M'} {s : Set M} {x : M} (hG : G.LocalInvariantProp G' P) (h : ChartedSpace.LiftPropWithinAt P g s x) (h₁ : ∀ y ∈ s, g' y = g y) (hx : g' x = g x) : ChartedSpace.LiftPropWithinAt P g' s x
• StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_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} {g g' : M → M'} {s : Set M} {x : M} (hG : G.LocalInvariantProp G' P) (h₁ : ∀ y ∈ s, g' y = g y) (hx : g' x = g x) : ChartedSpace.LiftPropWithinAt P g' s x ↔ ChartedSpace.LiftPropWithinAt P g s x
• StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_of_mem 📋 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} {g g' : M → M'} {s : Set M} {x : M} (hG : G.LocalInvariantProp G' P) (h : ChartedSpace.LiftPropWithinAt P g s x) (h₁ : ∀ y ∈ s, g' y = g y) (hx : x ∈ s) : ChartedSpace.LiftPropWithinAt P g' s x
• StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_iff_of_mem 📋 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} {g g' : M → M'} {s : Set M} {x : M} (hG : G.LocalInvariantProp G' P) (h₁ : ∀ y ∈ s, g' y = g y) (hx : x ∈ s) : ChartedSpace.LiftPropWithinAt P g' s x ↔ ChartedSpace.LiftPropWithinAt P g s x
• 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
• StructureGroupoid.LocalInvariantProp.liftPropOn_of_locally_liftPropOn 📋 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} {g : M → M'} {s : Set M} (hG : G.LocalInvariantProp G' P) (h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ ChartedSpace.LiftPropOn P g (s ∩ u)) : ChartedSpace.LiftPropOn P g s
• StructureGroupoid.LocalInvariantProp.liftPropAt_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} {x : M} {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) (hx : x ∈ e.source) : ChartedSpace.LiftPropAt Q (↑e) x
• StructureGroupoid.LocalInvariantProp.liftProp_subtype_val 📋 Mathlib.Geometry.Manifold.LocalInvariantProperties
  {H : Type u_1} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} {Q : (H → H) → Set H → H → Prop} (hG : G.LocalInvariantProp G Q) (hQ : ∀ (y : H), Q id Set.univ y) (U : TopologicalSpace.Opens M) : ChartedSpace.LiftProp Q Subtype.val
• StructureGroupoid.HasGroupoid.comp 📋 Mathlib.Geometry.Manifold.LocalInvariantProperties
  {H₁ : Type u_6} [TopologicalSpace H₁] {H₂ : Type u_7} [TopologicalSpace H₂] {H₃ : Type u_8} [TopologicalSpace H₃] [ChartedSpace H₁ H₂] [ChartedSpace H₂ H₃] {G₁ : StructureGroupoid H₁} [HasGroupoid H₂ G₁] [ClosedUnderRestriction G₁] (G₂ : StructureGroupoid H₂) [HasGroupoid H₃ G₂] (H : ∀ e ∈ G₂, ChartedSpace.LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e) e.source) : HasGroupoid H₃ G₁
• StructureGroupoid.LocalInvariantProp.left_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' → s ⊆ f ⁻¹' e'.source → f x ∈ e'.source → P f s x → P (↑e' ∘ f) s 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
• StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_target_aux2 📋 Mathlib.Geometry.Manifold.LocalInvariantProperties
  {H : Type u_1} {H' : Type u_3} {M' : Type u_4} [TopologicalSpace H] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {f : OpenPartialHomeomorph M' H'} {P : (H → H') → Set H → H → Prop} (hG : G.LocalInvariantProp G' P) (g : H → M') {x : H} {s : Set H} (hf : f ∈ StructureGroupoid.maximalAtlas M' G') (xf : g x ∈ f.source) (hgs : ContinuousWithinAt g s x) : P (↑(chartAt H' (g x)) ∘ g) s x ↔ P (↑f ∘ g) s x
• StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_target 📋 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'} {f : OpenPartialHomeomorph M' H'} {P : (H → H') → Set H → H → Prop} {g : M → M'} {s : Set M} {x : M} (hG : G.LocalInvariantProp G' P) (hf : f ∈ StructureGroupoid.maximalAtlas M' G') (xf : g x ∈ f.source) : ChartedSpace.LiftPropWithinAt P g s x ↔ ContinuousWithinAt g s x ∧ ChartedSpace.LiftPropWithinAt P (↑f ∘ g) s x
• StructureGroupoid.LocalInvariantProp.liftProp_inclusion 📋 Mathlib.Geometry.Manifold.LocalInvariantProperties
  {H : Type u_1} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} {Q : (H → H) → Set H → H → Prop} (hG : G.LocalInvariantProp G Q) (hQ : ∀ (y : H), Q id Set.univ y) {U V : TopologicalSpace.Opens M} (hUV : U ≤ V) : ChartedSpace.LiftProp Q (TopologicalSpace.Opens.inclusion hUV)
• 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)
• OpenPartialHomeomorph.isLocalStructomorphWithinAt_source_iff 📋 Mathlib.Geometry.Manifold.LocalInvariantProperties
  {H : Type u_1} [TopologicalSpace H] {G : StructureGroupoid H} [ClosedUnderRestriction G] (f : OpenPartialHomeomorph H H) {x : H} : G.IsLocalStructomorphWithinAt (↑f) f.source x ↔ x ∈ f.source → ∃ e ∈ G, e.source ⊆ f.source ∧ Set.EqOn (↑f) (↑e) e.source ∧ x ∈ e.source
• OpenPartialHomeomorph.isLocalStructomorphWithinAt_iff 📋 Mathlib.Geometry.Manifold.LocalInvariantProperties
  {H : Type u_1} [TopologicalSpace H] {G : StructureGroupoid H} [ClosedUnderRestriction G] (f : OpenPartialHomeomorph H H) {s : Set H} {x : H} (hx : x ∈ f.source ∪ sᶜ) : G.IsLocalStructomorphWithinAt (↑f) s x ↔ x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ Set.EqOn (↑f) (↑e) (s ∩ e.source) ∧ x ∈ e.source
• 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.liftPropAt_iff_comp_subtype_val 📋 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} (hG : G.LocalInvariantProp G' P) {U : TopologicalSpace.Opens M} (f : M → M') (x : ↥U) : ChartedSpace.LiftPropAt P f ↑x ↔ ChartedSpace.LiftPropAt P (f ∘ Subtype.val) 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)
• OpenPartialHomeomorph.isLocalStructomorphWithinAt_iff' 📋 Mathlib.Geometry.Manifold.LocalInvariantProperties
  {H : Type u_1} [TopologicalSpace H] {G : StructureGroupoid H} [ClosedUnderRestriction G] (f : OpenPartialHomeomorph H H) {s : Set H} {x : H} (hs : f.source ⊆ s) (hx : x ∈ f.source ∪ sᶜ) : G.IsLocalStructomorphWithinAt (↑f) s x ↔ x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ Set.EqOn (↑f) (↑e) e.source ∧ x ∈ e.source
• StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart 📋 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} {f : 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) (hf : f ∈ StructureGroupoid.maximalAtlas M' G') (xf : g x ∈ f.source) : ChartedSpace.LiftPropWithinAt P g s x ↔ ContinuousWithinAt g s x ∧ P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
• StructureGroupoid.LocalInvariantProp.liftPropOn_indep_chart 📋 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} {f : OpenPartialHomeomorph M' H'} {P : (H → H') → Set H → H → Prop} {g : M → M'} {s : Set M} (hG : G.LocalInvariantProp G' P) (he : e ∈ StructureGroupoid.maximalAtlas M G) (hf : f ∈ StructureGroupoid.maximalAtlas M' G') (h : ChartedSpace.LiftPropOn P g s) {y : H} (hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (s ∩ g ⁻¹' f.source)) : P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) y
• StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_target_aux 📋 Mathlib.Geometry.Manifold.LocalInvariantProperties
  {H : Type u_1} {H' : Type u_3} {M' : Type u_4} {X : Type u_5} [TopologicalSpace H] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] [TopologicalSpace X] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {f : OpenPartialHomeomorph M' H'} {P : (H → H') → Set H → H → Prop} (hG : G.LocalInvariantProp G' P) {g : X → M'} {e : OpenPartialHomeomorph X H} {x : X} {s : Set X} (xe : x ∈ e.source) (hf : f ∈ StructureGroupoid.maximalAtlas M' G') (xf : g x ∈ f.source) (hgs : ContinuousWithinAt g s x) : P (↑(chartAt H' (g x)) ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔ P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
• StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart' 📋 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} {f : 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) (hf : f ∈ StructureGroupoid.maximalAtlas M' G') (xf : g x ∈ f.source) : ChartedSpace.LiftPropWithinAt P g s x ↔ ContinuousWithinAt g s x ∧ ChartedSpace.LiftPropWithinAt P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
• StructureGroupoid.LocalInvariantProp.mk 📋 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} (is_local : ∀ {s : Set H} {x : H} {u : Set H} {f : H → H'}, IsOpen u → x ∈ u → (P f s x ↔ P f (s ∩ u) x)) (right_invariance' : ∀ {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)) (congr_of_forall : ∀ {s : Set H} {x : H} {f g : H → H'}, (∀ y ∈ s, f y = g y) → f x = g x → P f s x → P g s x) (left_invariance' : ∀ {s : Set H} {x : H} {f : H → H'} {e' : OpenPartialHomeomorph H' H'}, e' ∈ G' → s ⊆ f ⁻¹' e'.source → f x ∈ e'.source → P f s x → P (↑e' ∘ f) s x) : G.LocalInvariantProp G' P
• StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_aux' 📋 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} {f : 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) (hf : f ∈ StructureGroupoid.maximalAtlas M' G') (xf : g x ∈ f.source) (hgs : ContinuousWithinAt g s x) : P (↑(chartAt H' (g x)) ∘ g ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x) ↔ P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
• StructureGroupoid.LocalInvariantProp.liftPropAt_iff_comp_inclusion 📋 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} (hG : G.LocalInvariantProp G' P) {U V : TopologicalSpace.Opens M} (hUV : U ≤ V) (f : ↥V → M') (x : ↥U) : ChartedSpace.LiftPropAt P f (Set.inclusion hUV x) ↔ ChartedSpace.LiftPropAt P (f ∘ Set.inclusion hUV) x
• StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_aux 📋 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 e' : OpenPartialHomeomorph M H} {f f' : 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) (he' : e' ∈ StructureGroupoid.maximalAtlas M G) (xe' : x ∈ e'.source) (hf : f ∈ StructureGroupoid.maximalAtlas M' G') (xf : g x ∈ f.source) (hf' : f' ∈ StructureGroupoid.maximalAtlas M' G') (xf' : g x ∈ f'.source) (hgs : ContinuousWithinAt g s x) : P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔ P (↑f' ∘ g ∘ ↑e'.symm) (↑e'.symm ⁻¹' s) (↑e' x)
• contMDiffOn_of_mem_contDiffGroupoid 📋 Mathlib.Geometry.Manifold.ContMDiff.Atlas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {e' : OpenPartialHomeomorph H H} (h : e' ∈ contDiffGroupoid n I) : ContMDiffOn I I n (↑e') e'.source
• symm_trans_trans_mem_contDiffGroupoid_of_contMDiffOn 📋 Mathlib.Geometry.Manifold.ContMDiff.Atlas
  {𝕜 : 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] [ChartedSpace H M] {n : WithTop ℕ∞} {ϕ ϕ' : OpenPartialHomeomorph M H} (hϕ : ϕ ∈ IsManifold.maximalAtlas I n M) (hϕ' : ϕ' ∈ IsManifold.maximalAtlas I n M) {f : OpenPartialHomeomorph M M} (hf : ContMDiffOn I I n (↑f) f.source) (hf' : ContMDiffOn I I n (↑f.symm) f.target) : ϕ.symm.trans (f.trans ϕ') ∈ contDiffGroupoid n I
• contMDiffFiberwiseLinear 📋 Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
  {𝕜 : Type u_1} (B : Type u_2) (F : Type u_3) [TopologicalSpace B] [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {EB : Type u_4} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_5} [TopologicalSpace HB] [ChartedSpace HB B] (IB : ModelWithCorners 𝕜 EB HB) (n : WithTop ℕ∞) : StructureGroupoid (B × F)
• mem_contMDiffFiberwiseLinear_iff 📋 Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
  {𝕜 : Type u_1} (B : Type u_2) (F : Type u_3) [TopologicalSpace B] [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {EB : Type u_4} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_5} [TopologicalSpace HB] [ChartedSpace HB B] (IB : ModelWithCorners 𝕜 EB HB) {n : WithTop ℕ∞} (e : OpenPartialHomeomorph (B × F) (B × F)) : e ∈ contMDiffFiberwiseLinear B F IB n ↔ ∃ φ U, ∃ (hU : IsOpen U) (hφ : ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun x => ↑(φ x)) U) (h2φ : ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun x => ↑(φ x).symm) U), e.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)
• conformalGroupoid 📋 Mathlib.Geometry.Manifold.ConformalGroupoid
  {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] : StructureGroupoid X
• TopCat.of.hasGroupoid 📋 Mathlib.Geometry.Manifold.Sheaf.Basic
  {H : Type u_1} [TopologicalSpace H] {G : StructureGroupoid H} (M : Type u) [TopologicalSpace M] [ChartedSpace H M] [HasGroupoid M G] : HasGroupoid (↑(TopCat.of M)) G
• StructureGroupoid.LocalInvariantProp.sheaf 📋 Mathlib.Geometry.Manifold.Sheaf.Basic
  {H : Type u_1} [TopologicalSpace H] {H' : Type u_2} [TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} (M : Type u) [TopologicalSpace M] [ChartedSpace H M] (M' : Type u) [TopologicalSpace M'] [ChartedSpace H' M'] (hG : G.LocalInvariantProp G' P) : TopCat.Sheaf (Type u) (TopCat.of M)
• StructureGroupoid.LocalInvariantProp.localPredicate 📋 Mathlib.Geometry.Manifold.Sheaf.Basic
  {H : Type u_1} [TopologicalSpace H] {H' : Type u_2} [TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} (M : Type u) [TopologicalSpace M] [ChartedSpace H M] (M' : Type u) [TopologicalSpace M'] [ChartedSpace H' M'] (hG : G.LocalInvariantProp G' P) : TopCat.LocalPredicate fun x => M'
• StructureGroupoid.LocalInvariantProp.sheafHasCoeToFun 📋 Mathlib.Geometry.Manifold.Sheaf.Basic
  {H : Type u_1} [TopologicalSpace H] {H' : Type u_2} [TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} (M : Type u) [TopologicalSpace M] [ChartedSpace H M] (M' : Type u) [TopologicalSpace M'] [ChartedSpace H' M'] (hG : G.LocalInvariantProp G' P) (U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ) : CoeFun ((StructureGroupoid.LocalInvariantProp.sheaf M M' hG).obj.obj U) fun x => ↥(Opposite.unop U) → M'
• StructureGroupoid.LocalInvariantProp.section_spec 📋 Mathlib.Geometry.Manifold.Sheaf.Basic
  {H : Type u_1} [TopologicalSpace H] {H' : Type u_2} [TopologicalSpace H'] {G : StructureGroupoid H} {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop} (M : Type u) [TopologicalSpace M] [ChartedSpace H M] (M' : Type u) [TopologicalSpace M'] [ChartedSpace H' M'] (hG : G.LocalInvariantProp G' P) (U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ) (f : (StructureGroupoid.LocalInvariantProp.sheaf M M' hG).obj.obj U) : ChartedSpace.LiftProp P ↑f

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 ce5dd8c