range_eq_of_proj — Mathlib

English

If f: E → p satisfies f(x)=x for all x in p, then the range of f is the whole space: range f = ⊤.

Русский

Если отображение f: E → p удовлетворяет f(x)=x для всех x в p, то образ равен всему пространству: range f = ⊤.

LaTeX

$$$\\operatorname{range} f = \\top$$$

Lean4

theorem range_eq_of_proj {f : E →ₗ[R] p} (hf : ∀ x : p, f x = x) : range f = ⊤ :=
  range_eq_top.2 fun x => ⟨x, hf x⟩

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