pairwiseDisjoint_range_iff — Mathlib

English

For f : α → Set β, the pairwise disjointness of its range is equivalent to a condition on all pairs x,y with f x ≠ f y.

Русский

Для любого f: α → Set β попарность образа диапазона эквивалентна условию на все пары x,y если f x ≠ f y.

LaTeX

$$ (range f).PairwiseDisjoint id \\iff ∀ x y, f x ≠ f y → Disjoint (f x) (f y) $$

Lean4

theorem pairwiseDisjoint_range_iff {α β : Type*} {f : α → (Set β)} :
    (range f).PairwiseDisjoint id ↔ ∀ x y, f x ≠ f y → Disjoint (f x) (f y) := by
  aesop (add simp [PairwiseDisjoint, Set.Pairwise])

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