linearIndepOn_sUnion_of_directed — Mathlib

English

Let s be a family of sets of ι directed by inclusion, and suppose each a in s is linearly independent with respect to v. Then the union s⋃ is linearly independent with respect to v.

Русский

Пусть s — семейство подмножеств ι, направленный по включению, и пусть для каждого a ∈ s множество {v|_a} линейно независимо. Тогда объединение s⋃ линейно независимо по отношению к v.

LaTeX

$$$(\\forall a \\in s,\\ LinearIndepOn_R(v, a)) \\Rightarrow \\ LinearIndepOn_R(v, \\bigcup a \\in s, a)$$$

Lean4

theorem linearIndepOn_sUnion_of_directed {s : Set (Set ι)} (hs : DirectedOn (· ⊆ ·) s)
    (h : ∀ a ∈ s, LinearIndepOn R v a) : LinearIndepOn R v (⋃₀ s) :=
  by
  rw [sUnion_eq_iUnion]
  exact linearIndepOn_iUnion_of_directed hs.directed_val (by simpa using h)

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