of_comp_of_surjective — Mathlib

English

If hr is Pairwise (r on f) and f is surjective, then r holds pairwise.

Русский

Если hr держит попарно через f, и f сюръективна, то r держится попарно.

LaTeX

$$$\\operatorname{Pairwise}(r\\ on\\ f) \\land \\operatorname{Surjective}(f) \\Rightarrow \\operatorname{Pairwise}(r)$$$

Lean4

theorem of_comp_of_surjective {f : β → α} (hr : Pairwise (r on f)) (hf : Surjective f) : Pairwise r :=
  hf.forall₂.2 fun _ _ h ↦ hr <| ne_of_apply_ne f h

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