Theorems · Theorem · order theory

preimage_find_eq_disjointed

∀ {α : Type u_1} (s : ℕ → Set α) (H : ∀ (x : α), ∃ n, x ∈ s n) [inst : (x : α) → (n : ℕ) → Decidable (x ∈ s n)] (n : ℕ),
  (fun x => Nat.find ⋯) ⁻¹' {n} = disjointed s n

Defined in

Mathlib.Order.Disjointed

Cited by

2 results in Mathlib

Foundations

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

Assumes

Decidable