Theorems · Theorem · order theory

InfClosed.biInf_mem_of_nonempty

∀ {α : Type u_3} [inst : CompleteLattice α] {s : Set α} {ι : Type u_5} {t : Set ι} {f : ι → α},
  InfClosed s → t.Finite → t.Nonempty → (∀ i ∈ t, f i ∈ s) → ⨅ i ∈ t, f i ∈ s

Defined in

Mathlib.Order.SupClosed

Cited by

1 results in Mathlib

Foundations

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

Assumes

CompleteLattice