list_wbtw_map_iff — Mathlib

English

From Sbtw, one obtains that the list is pairwise with non-equality: l.Pairwise (fun x1 x2 => x1 ≠ x2).

Русский

Из Sbtw следует, что список попарно несодержащий равенства элементов: l.Pairwise(≠).

LaTeX

$$$l.Sbtw(R) \\Rightarrow l.Pairwise(\\neq)\\,$$$

Lean4

theorem _root_.Function.Injective.list_wbtw_map_iff {l : List P} {f : P →ᵃ[R] P'} (hf : Function.Injective f) :
    (l.map f).Wbtw R ↔ l.Wbtw R :=
  ⟨fun h ↦ h.of_map hf.wbtw_map_iff.1, fun h ↦ h.map f⟩

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