restr_source_inter — Mathlib

English

Restricting to e.source ∩ s is the same as restricting to s when considering the restricted map: e.restr (e.source ∩ s) = e.restr s.

Русский

Ограничение до e.source ∩ s эквивалентно ограничению до s для соответствующей карты: e.restr (e.source ∩ s) = e.restr s.

LaTeX

$$e.restr (e.source ∩ s) = e.restr s$$

Lean4

theorem restr_source_inter (s : Set X) : e.restr (e.source ∩ s) = e.restr s :=
  by
  refine OpenPartialHomeomorph.ext _ _ (fun x => rfl) (fun x => rfl) ?_
  simp [e.open_source.interior_eq, ← inter_assoc]

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