restr — Mathlib

English

Restriction respects equivalence: if e ≈ e', then e.restr s ≈ e'.restr s for any s.

Русский

Ограничение сохраняет эквивалентность: если e ≈ e', то e.restr s ≈ e'.restr s для любого s.

LaTeX

$$$ (e \\approx e') \\Rightarrow (e.restr s) \\approx (e'.restr s)$$$

Lean4

/-- Restriction of partial equivs respects equivalence. -/
theorem restr {e e' : PartialEquiv α β} (he : e ≈ e') (s : Set α) : e.restr s ≈ e'.restr s :=
  by
  constructor
  · simp [he.1]
  · intro x hx
    simp only [mem_inter_iff, restr_source] at hx
    exact he.2 hx.1

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