finsetInf'_mem — Mathlib

English

Let s be InfClosed. For a nonempty Finset t and a family f, if f(i) ∈ s for all i in t, then t.inf' ht f ∈ s.

Русский

Пусть s удовлетворяет InfClosed. Пусть t — непустой конечный набор индексов, и для всех i в t выполняется f(i) ∈ s; тогда t.inf' ht f ∈ s.

LaTeX

$$$\\forall \\alpha\\ [\\text{SemilatticeInf } \\alpha],\\ s:\\ Set\\ \\alpha,\\t:\\ Finset\\ ι,\\ f:\\ ι \\to α,\\ InfClosed\\ s \\Rightarrow t.Nonempty \\to (\\forall i, i\\in t \\Rightarrow f(i) \\in s) \\Rightarrow t.inf'_ht\\ f \\in s$$$

Lean4

theorem finsetInf'_mem (hs : InfClosed s) (ht : t.Nonempty) : (∀ i ∈ t, f i ∈ s) → t.inf' ht f ∈ s :=
  inf'_induction _ _ hs

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