inf'_mem — Mathlib

English

If two finite sets s and t are equal and the functions f and g agree on s, then the infimum over s with f equals the infimum over t with g.

Русский

Если множества s и t равны и функции f и g совпадают на s, то инфимума над s с f равна инфимума над t с g.

LaTeX

$$$s = t \\Rightarrow s.inf' H f = t.inf' (h_1 \\;\\text{▸} \\; H) g \\text{ whenever } \\forall x \\in s, f(x)=g(x)$$$

Lean4

theorem inf'_mem (s : Set α) (w : ∀ᵉ (x ∈ s) (y ∈ s), x ⊓ y ∈ s) {ι : Type*} (t : Finset ι) (H : t.Nonempty) (p : ι → α)
    (h : ∀ i ∈ t, p i ∈ s) : t.inf' H p ∈ s :=
  inf'_induction H p w h

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