list_wbtw_map_iff — Mathlib

English

If l is a list and f is an affine equivalence, then mapping l by f preserves Wbtw: (l.map f).Wbtw R ↔ l.Wbtw R.

Русский

Если l — список, а f — аффинное эквивалентное отображение, то отображение л by f сохраняет Wbtw: (l.map f).Wbtw R ⇔ l.Wbtw R.

LaTeX

$$$(l.map f).Wbtw(R) \\iff l.Wbtw(R)$$$

Lean4

theorem _root_.AffineEquiv.list_wbtw_map_iff {l : List P} (f : P ≃ᵃ[R] P') : (l.map f).Wbtw R ↔ l.Wbtw R :=
  by
  have hf : Function.Injective f.toAffineMap := f.injective
  apply hf.list_wbtw_map_iff

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