trans_ofSet — Mathlib

English

Composing with the identity on an open set s from the left yields the restriction to the preimage of s.

Русский

Слева композиция с идентичностью на открытом множестве s равна ограничению до его предобраза.

LaTeX

$$$ e.trans(\\mathrm{ofSet}(s, hs)) = e.restr (e^{-1}'s) $$$

Lean4

theorem trans_ofSet {s : Set Y} (hs : IsOpen s) : e.trans (ofSet s hs) = e.restr (e ⁻¹' s) :=
  OpenPartialHomeomorph.ext _ _ (fun _ => rfl) (fun _ => rfl) <| by
    rw [trans_source, restr_source, ofSet_source, ← preimage_interior, hs.interior_eq]

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