Theorems · Theorem · order theory

disjoint_memPartition

∀ {α : Type u_1} (f : ℕ → Set α) (n : ℕ) {u v : Set α},
  u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v

Defined in

Mathlib.Data.Set.MemPartition

Cited by

3 results in Mathlib

Foundations

Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound