Theorems · Theorem · order theory

CountableInfClosed.iInf_mem

∀ {ι : Sort u_1} {α : Type u_2} {s : Set α} [inst : CompleteLattice α] [Countable ι] [Nonempty ι],
  CountableInfClosed s → ∀ {A : ι → α}, (∀ (n : ι), A n ∈ s) → ⨅ n, A n ∈ s

Defined in

Mathlib.Order.CountableSupClosed

Cited by

3 results in Mathlib

Foundations

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

Assumes

CompleteLatticeCountableNonempty