symm_trans_self — Mathlib

English

The composition of a partial inverse with its forward map is the partial identity on the codomain of the inverse.

Русский

Сочетание обратной частичной эквивалентности и её композиции с оригиналом даёт частичное тождество на кодоменной части обратной.

LaTeX

$$f.symm trans f = \\operatorname{ofSet} \\{b \\mid (f.symm b).isSome\\}$$

Lean4

theorem symm_trans_self (f : α ≃. β) : f.symm.trans f = ofSet {b | (f.symm b).isSome} :=
  symm_injective <| by simp [symm_trans_rev, self_trans_symm, -symm_symm]

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