union_of_quotient — Mathlib

English

If s and t are disjoint, then linearIndepOn f s ∪ t is equivalent to linearIndepOn f s and linearIndepOn (mkQ ... ) t.

Русский

Если s и t непересекаются, то линейная независимость на s ∪ t эквивалентна независимости на s и независимости на t после взятия фактор-модуля.

LaTeX

$$$ \text{LinearIndepOn}_R f (s \cup t) \quad\Leftrightarrow\quad \text{LinearIndepOn}_R f s \;\wedge\; \text{LinearIndepOn}_R (\mathrm{mkQ} (\mathrm{span}_R (f'' s)) \circ f) t $$$

Lean4

theorem union_of_quotient {s t : Set ι} {f : ι → M} (hs : LinearIndepOn R f s)
    (ht : LinearIndepOn R (mkQ (span R (f '' s)) ∘ f) t) : LinearIndepOn R f (s ∪ t) :=
  by
  apply hs.union ht.of_comp
  convert (Submodule.range_ker_disjoint ht).symm
  · simp
  aesop

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