isLinearSet_iff_exists_fg_eq_vadd

English

IsLinearSet s iff there exists a ∈ M and FG P ⊆ M with s = a +ᵥ P.

Русский

IsLinearSet s эквивалентно существованию a и FG P, таких что s = a +ᵥ P.

LaTeX

$$$ IsLinearSet s \\iff \\exists a \\exists P, P.FG \\wedge s = a +ᵥ (P : Set M) $$$

Lean4

theorem isLinearSet_iff_exists_fg_eq_vadd :
    IsLinearSet s ↔ ∃ (a : M) (P : AddSubmonoid M), P.FG ∧ s = a +ᵥ (P : Set M) :=
  isLinearSet_iff.trans
    (exists_congr fun a => ⟨fun ⟨t, hs⟩ => ⟨_, ⟨t, rfl⟩, hs⟩, fun ⟨P, ⟨t, hP⟩, hs⟩ => ⟨t, by rwa [hP]⟩⟩)

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