Theorems · Theorem · order theory

InfClosed.biInf_mem

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

Defined in

Mathlib.Order.SupClosed

Cited by

2 results in Mathlib

Foundations

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

Assumes

CompleteLattice