pairwise_comp — Mathlib

English

If x lies in the source, then e x lies in the target.

Русский

Если x принадлежит области определения, то e x принадлежит области значения.

LaTeX

$$$\forall x (h:\, x \in e.\mathrm{source}),\ e(x) \in e.\mathrm{target}$$$

Lean4

theorem pairwise_comp {X : Type*} {Y : Type*} {F} [FunLike F Y X] [EmbeddingLike F Y X] (f : F) {p : X → X → Prop}
    (h : Pairwise p) : Pairwise (p on f) :=
  h.comp_of_injective <| EmbeddingLike.injective f

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