trans_refl_restr — Mathlib

English

The composition of e with the restriction of the identity on s equals the restriction of e to e^{-1}(s).

Русский

Сочетание e с ограничением тождества на s равно ограничению e до e^{-1}(s).

LaTeX

$$$e.\mathrm{trans}((\mathrm{PartialEquiv.refl}\,\mathrm{β}).\mathrm{restr}\,s) = e.\mathrm{restr}(e^{-1}(s))$$$

Lean4

theorem trans_refl_restr (s : Set β) : e.trans ((PartialEquiv.refl β).restr s) = e.restr (e ⁻¹' s) :=
  PartialEquiv.ext (fun _ => rfl) (fun _ => rfl) (by simp [trans_source])

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