list_sbtw_map_iff — Mathlib

English

If l is Sbtw and f is an injective affine map, then mapping l via f preserves the Sbtw relation: (l.map f).Sbtw R ↔ l.Sbtw R.

Русский

Если l удовлетворяет Sbtw и f — инъективное аффинное отображение, то отображение l через f сохраняет Sbtw: (l.map f).Sbtw R ⇔ l.Sbtw R.

LaTeX

$$$(l.map f).Sbtw(R) \\iff l.Sbtw(R)$ (при инъективности f).$$

Lean4

theorem _root_.Function.Injective.list_sbtw_map_iff {l : List P} {f : P →ᵃ[R] P'} (hf : Function.Injective f) :
    (l.map f).Sbtw R ↔ l.Sbtw R := by
  rw [List.Sbtw, List.Sbtw, hf.list_wbtw_map_iff]
  refine ⟨fun ⟨hl, hp⟩ ↦ ⟨hl, hp.of_map _ ?_⟩, fun ⟨hl, hp⟩ ↦ ⟨hl, hp.map _ ?_⟩⟩ <;> simp [hf.ne_iff]

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