exists_smul_add_of_span_sup_eq_top

English

Assume (R · x) ⊔ I = ⊤. Then for every y ∈ L there exist t ∈ R and z ∈ I such that y = t·x + z.

Русский

Пусть выполняется (R · x) ⊔ I = ⊤. Тогда для каждого y ∈ L существуют t ∈ R и z ∈ I такие, что y = t·x + z.

LaTeX

$$$\bigl((R \cdot x) \sqcup I = \top\bigr) \Rightarrow \forall y \in L, \exists t \in R, \exists z \in I: y = t \cdot x + z$$$

Lean4

theorem exists_smul_add_of_span_sup_eq_top (y : L) : ∃ t : R, ∃ z ∈ I, y = t • x + z :=
  by
  have hy : y ∈ (⊤ : Submodule R L) := Submodule.mem_top
  simp only [← hxI, Submodule.mem_sup, Submodule.mem_span_singleton] at hy
  obtain ⟨-, ⟨t, rfl⟩, z, hz, rfl⟩ := hy
  exact ⟨t, z, hz, rfl⟩

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