linearIndepOn_congr — Mathlib

English

If w is equal to v on s, then LinearIndepOn R v s is equivalent to LinearIndepOn R w s.

Русский

Если w совпадает с v на s, то независимость сохраняется: LinearIndepOn R v s ⇔ LinearIndepOn R w s.

LaTeX

$$LinearIndepOn R v s ↔ LinearIndepOn R w s when v ≡ w on s$$

Lean4

theorem linearIndepOn_congr {w : ι → M} (h : EqOn v w s) : LinearIndepOn R v s ↔ LinearIndepOn R w s :=
  by
  rw [LinearIndepOn, LinearIndepOn]
  convert Iff.rfl using 2
  ext x
  exact h.symm x.2

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