Theorems · Definition · logic and foundations

Set.PairwiseDisjoint

{α : Type u_1} → {ι : Type u_4} → [inst : PartialOrder α] → [OrderBot α] → Set ι → (ι → α) → Prop

A set is PairwiseDisjoint under f, if the images of any distinct two elements under f are disjoint. s.Pairwise Disjoint is (definitionally) the same as s.PairwiseDisjoint id. We prefer the latter in order to allow dot notation on Set.PairwiseDisjoint, even though the former unfolds more nicely.

Defined in

Mathlib.Data.Set.Pairwise.Basic

Cited by

275 results in Mathlib

Foundations

Depth 5 from the axioms, rests on 24 definitions · uses no axioms

Assumes

PartialOrderOrderBot