symm_comp_self — Mathlib

English

A Continuous Linear Equivalence e is surjective; hence e is bijective with inverse e.symm.

Русский

Пусть e — непрерывная линейная эквивалентность; она сюръективна и потому биективна с обратным e.symm.

LaTeX

$$$\\operatorname{Surjective}(e) \\land \\operatorname{Bijective}(e)$$$

Lean4

@[simp]
theorem symm_comp_self (e : M₁ ≃SL[σ₁₂] M₂) : (e.symm : M₂ → M₁) ∘ (e : M₁ → M₂) = id :=
  by
  ext x
  exact symm_apply_apply e x

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