right_invariance — Mathlib

English

Right invariance with open partial homeomorphs preserves P under composition with f.

Русский

Правая инвариантность сохраняет P при композиции с f и открытыми частичными гомоморфами.

LaTeX

$$$P (f \circ e.symm) (s) x \iff P f s x$$$

Lean4

theorem right_invariance {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 :=
  by
  refine ⟨fun h ↦ ?_, hG.right_invariance' he hxe⟩
  have := hG.right_invariance' (G.symm he) (e.mapsTo hxe) h
  rw [e.symm_symm, e.left_inv hxe] at this
  refine hG.congr ?_ ((hG.congr_set ?_).mp this)
  · refine eventually_of_mem (e.open_source.mem_nhds hxe) fun x' hx' ↦ ?_
    simp_rw [Function.comp_apply, e.left_inv hx']
  · rw [eventuallyEq_set]
    refine eventually_of_mem (e.open_source.mem_nhds hxe) fun x' hx' ↦ ?_
    simp_rw [mem_preimage, e.left_inv hx']

Похожие утверждения