affineIndependent_equiv — Mathlib

English

If there is an equivalence between index types, affine independence is preserved under composition with the equivalence.

Русский

Если между индексными множествами есть биекция, аффинная независимость сохраняется после композиции с биекцией.

LaTeX

$$AffineIndependent k (p ∘ e) ↔ AffineIndependent k p$$

Lean4

theorem affineIndependent_equiv {ι' : Type*} (e : ι ≃ ι') {p : ι' → P} :
    AffineIndependent k (p ∘ e) ↔ AffineIndependent k p :=
  by
  refine ⟨?_, AffineIndependent.comp_embedding e.toEmbedding⟩
  intro h
  have : p = p ∘ e ∘ e.symm.toEmbedding := by
    ext
    simp
  rw [this]
  exact h.comp_embedding e.symm.toEmbedding

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