mem_add — Mathlib

English

If two projective points [v] and [w] lie in a subspace T, and v,w,v+w are nonzero, then [v+w] lies in T.

Русский

Пусть две точки [v] и [w] принадлежат подпространству T, и v, w, v+w непущи нулю, тогда [v+w] принадлежит T.

LaTeX

$$$( [v] \in T ) \land ( [w] \in T ) \land ( v+w \neq 0 ) \Rightarrow ( [v+w] \in T )$$$

Lean4

theorem mem_add (T : Subspace K V) (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0) :
    Projectivization.mk K v hv ∈ T → Projectivization.mk K w hw ∈ T → Projectivization.mk K (v + w) hvw ∈ T :=
  T.mem_add' v w hv hw hvw

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