on_injective — Mathlib

English

If s.Pairwise r, f is injective, and ∀ x, f x ∈ s, then r on f is pairwise.

Русский

Если s.Pairwise r, f инъективна и ∀ x, f x ∈ s, то r на f попарно.

LaTeX

$$$\\operatorname{Set.Pairwise}(s,r) \\land \\operatorname{Injective}(f) \\land \\forall x, f(x) \\in s \\Rightarrow \\operatorname{Pairwise}(r\\ on\\ f)$$$

Lean4

theorem on_injective (hs : s.Pairwise r) (hf : Function.Injective f) (hfs : ∀ x, f x ∈ s) : Pairwise (r on f) :=
  fun i j hij => hs (hfs i) (hfs j) (hf.ne hij)

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