union_id_of_quotient — Mathlib

English

If Disjoint s t, then LinearIndepOn R f (s ∪ t) is equivalent to LinearIndepOn R f s and LinearIndepOn R (mkQ ... ) t.

Русский

Если Disjoint s t, то LinearIndepOn R f (s ∪ t) эквивалентно LinearIndepOn R f s и LinearIndepOn R (mkQ ... ) t.

LaTeX

$$$\text{LinearIndepOn}_R f (s \cup t) \iff \text{LinearIndepOn}_R f s \land \text{LinearIndepOn}_R (\mathrm{mkQ} (\mathrm{span}_R (f'' s)) \circ f) t$$$

Lean4

theorem union_id_of_quotient {M' : Submodule R M} {s : Set M} (hs : s ⊆ M') (hs' : LinearIndepOn R id s) {t : Set M}
    (ht : LinearIndepOn R (mkQ M') t) : LinearIndepOn R id (s ∪ t) :=
  hs'.union_of_quotient <| by
    rw [image_id]
    exact ht.of_comp ((span R s).mapQ M' (LinearMap.id) (span_le.2 hs))

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