pairwise_comp_iff — Mathlib

English

If f is bijective, then Pairwise (on f) is equivalent to Pairwise on the domain.

Русский

Если f биективна, то попарность через f эквивалентна попарности на исходном множестве.

LaTeX

$$$\\operatorname{Bijective}(f) \\Rightarrow (\\operatorname{Pairwise}(r\\ on\\ f) \\iff \\operatorname{Pairwise}(r))$$$

Lean4

theorem pairwise_comp_iff {f : β → α} (hf : Bijective f) : Pairwise (r on f) ↔ Pairwise r :=
  ⟨fun hr ↦ hr.of_comp_of_surjective hf.surjective, fun hr ↦ hr.comp_of_injective hf.injective⟩

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