pairwise_iff_exists_forall — Mathlib

English

If s is nonempty, then s.Pairwise (Function.onFun r f) is equivalent to existence of a z such that ∀ x, if x ∈ s then r (f x) z.

Русский

Если s непусто, то s.Pairwise (функциональная композиция) эквивалентно существованию z, такого что для всех x ∈ s выполнено r (f x) z.

LaTeX

$$$[Nonempty \iota] (s : Set \alpha) (f : \alpha \to \iota) {r : \iota \to \iota \to \mathrm{Prop}} : s.Pairwise (r on f) \leftrightarrow \exists z, \forall x ∈ s, r (f x) z$$$

Lean4

theorem pairwise_iff_exists_forall [Nonempty ι] (s : Set α) (f : α → ι) {r : ι → ι → Prop} [IsEquiv ι r] :
    s.Pairwise (r on f) ↔ ∃ z, ∀ x ∈ s, r (f x) z :=
  by
  rcases s.eq_empty_or_nonempty with (rfl | hne)
  · simp
  · exact hne.pairwise_iff_exists_forall

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