quotient_iff_union — Mathlib

English

If s and t are disjoint, LinearIndepOn R f (s ∪ t) is equivalent to LinearIndepOn R f s ∧ LinearIndepOn R (comp mkQ f) t.

Русский

Если s и t непересекаются, LinearIndepOn R f (s ∪ t) эквивалентно LinearIndepOn R f s и LinearIndepOn R (comp mkQ f) t.

LaTeX

$$$\text{LinearIndepOn}_R f (s \cup t) \iff \text{LinearIndepOn}_R f s \land \text{LinearIndepOn}_R (\mathrm{comp} \; \mathrm{mkQ} \; f) t$$$

Lean4

theorem quotient_iff_union {s t : Set ι} {f : ι → M} (hs : LinearIndepOn R f s) (hst : Disjoint s t) :
    LinearIndepOn R (mkQ (span R (f '' s)) ∘ f) t ↔ LinearIndepOn R f (s ∪ t) := by
  rw [linearIndepOn_union_iff_quotient hst, and_iff_right hs]

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