self_trans_symm — Mathlib

English

The composition of a partial equivalence with its inverse is the partial identity on its domain.

Русский

Сочетание частичной эквивалентности и её обратной даёт частичное тождество на области определения функции.

LaTeX

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

Lean4

theorem self_trans_symm (f : α ≃. β) : f.trans f.symm = ofSet {a | (f a).isSome} :=
  by
  ext
  dsimp [PEquiv.trans]
  simp only [eq_some_iff f, Option.isSome_iff_exists, bind_eq_some_iff, ofSet_eq_some_iff]
  constructor
  · rintro ⟨b, hb₁, hb₂⟩
    exact ⟨PEquiv.inj _ hb₂ hb₁, b, hb₂⟩
  · simp +contextual

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