finsetInf'_mem_infClosure — Mathlib

English

Let t be a nonempty finite index set and f: t → α with f(i) ∈ s for all i ∈ t. Then the infimum t.inf'(ht) f lies in infClosure(s).

Русский

Пусть t — ненулевой конечный индексный набор и f: t → α так, что для каждого i ∈ t выполняется f(i) ∈ s. Тогда t.inf'(ht) f ∈ infClosure(s).

LaTeX

$$$t.NONEMPTY \to (\forall i \in t, f(i) \in s) \to t.inf' ht f \in \infClosure s$$$

Lean4

theorem finsetInf'_mem_infClosure {ι : Type*} {t : Finset ι} (ht : t.Nonempty) {f : ι → α} (hf : ∀ i ∈ t, f i ∈ s) :
    t.inf' ht f ∈ infClosure s :=
  infClosed_infClosure.finsetInf'_mem _ fun _i hi ↦ subset_infClosure <| hf _ hi

Похожие утверждения