ofTop_symm_apply — Mathlib

English

A linear equivalence induces an equivalence between the original module and its range, when the range is top.

Русский

Линейная эквивалентность порождает эквивалентность между модулем и его образом, когда образ совпадает с верхом.

LaTeX

$$theorem range : LinearMap.range (e : M →ₛₗ[σ₁₂] M₂) = ⊤$$

Lean4

theorem ofTop_symm_apply {h} (x : M) : (ofTop p h).symm x = ⟨x, h.symm ▸ trivial⟩ :=
  rfl

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