linearIndepOn_biUnion_of_directed

English

If each a in s has LinearIndepOn v (t a), then the union over a ∈ s of t a yields LinearIndepOn v (⋃ a ∈ s, t a).

Русский

Если для каждого a в s выполняется LinearIndepOn v (t a), то объединение по a ∈ s множества t a даёт линейную независимость LinearIndepOn v (⋃ a ∈ s, t a).

LaTeX

$$$(\\forall a\\in s,\\ LinearIndepOn_R(v, t(a))) \\Rightarrow \\ LinearIndepOn_R(v, \\bigcup_{a\\in s} t(a))$$$

Lean4

theorem linearIndepOn_biUnion_of_directed {η} {s : Set η} {t : η → Set ι} (hs : DirectedOn (t ⁻¹'o (· ⊆ ·)) s)
    (h : ∀ a ∈ s, LinearIndepOn R v (t a)) : LinearIndepOn R v (⋃ a ∈ s, t a) :=
  by
  rw [biUnion_eq_iUnion]
  exact linearIndepOn_iUnion_of_directed (directed_comp.2 <| hs.directed_val) (by simpa using h)

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