English
If s is a set containing top and closed under inf, then for any finite t and any p, if p(i) ∈ s for all i ∈ t, then t.inf p ∈ s.
Русский
Если s содержит верхнюю грань и замкнута относительно инф, то для любого конечного множества t и функции p: t → α, если p(i) ∈ s для всех i ∈ t, то inf_{i∈t} p(i) ∈ s.
LaTeX
$$$ s \\text{ is a set with } ⊤ \\in s \\text{ and closed under } \\inf \\; \\Rightarrow \\; (\\forall t\\ (\\forall i \\in t, p(i) \\in s) \\Rightarrow t.\\inf p \\in s)$$$
Lean4
theorem inf_mem (s : Set α) (w₁ : ⊤ ∈ s) (w₂ : ∀ᵉ (x ∈ s) (y ∈ s), x ⊓ y ∈ s) {ι : Type*} (t : Finset ι) (p : ι → α)
(h : ∀ i ∈ t, p i ∈ s) : t.inf p ∈ s :=
@inf_induction _ _ _ _ _ _ (· ∈ s) w₁ w₂ h
