mem_mul_span_singleton — Mathlib

English

For P ⊆ A and y ∈ A, x ∈ P · span{y} iff ∃ z ∈ P with z·y = x.

Русский

Для P и y: x ∈ P · span{y} эквивалентно существованию z ∈ P такого что z·y = x.

LaTeX

$$$x \\in P \\cdot \\operatorname{span} R\\{y\\} \\iff \\exists z \\in P, z \\cdot y = x$$$

Lean4

theorem mem_mul_span_singleton {x y : A} : x ∈ P * span R { y } ↔ ∃ z ∈ P, z * y = x := by
  simp_rw [mul_eq_map₂, map₂_span_singleton_eq_map_flip, mem_map, LinearMap.flip_apply, LinearMap.mul_apply_apply]

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