pairwise_comp_iff — Mathlib

English

If p is pairwise on X and f : X → Y is injective, then p is pairwise on X after applying f, i.e., p on f holds on X.

Русский

Если p парное отношение на X и f : X → Y инъекционна, то p на f сохраняется: p (f x) (f y) при x ≠ y.

LaTeX

$$$\text{Injective}(f) \wedge \operatorname{Pairwise} p \;\Rightarrow\; \operatorname{Pairwise}(p \text{ on } f)$$$

Lean4

theorem pairwise_comp_iff {X : Type*} {Y : Type*} {F} [EquivLike F Y X] (f : F) (p : X → X → Prop) :
    Pairwise (p on f) ↔ Pairwise p :=
  (EquivLike.bijective f).pairwise_comp_iff

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