restr_trans — Mathlib

English

For partial equivalences e: α ⇄ β and e': β ⇄ γ and a subset s ⊆ α, the restriction of e to s, followed by composition with e', equals the restriction of the composition e ∘ e' to s.

Русский

Для частичных эквивалентов e: α ⇄ β и e': β ⇄ γ и подмножества s ⊆ α, ограничение e на s, далее композиция с e', эквивалентно ограничению составления e ∘ e' на s.

LaTeX

$$$ (e.restr s) \\trans e' = (e \\trans e').restr s $$$

Lean4

theorem restr_trans (s : Set α) : (e.restr s).trans e' = (e.trans e').restr s :=
  PartialEquiv.ext (fun _ => rfl) (fun _ => rfl) <| by simp [trans_source, inter_comm, inter_assoc]

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