iInf_insert_update — Mathlib

English

Let x ∈ α, t Finset α, f: α → β, and hx: x ∉ t. Then the infimum over insert x t of update f x s i equals the infimum of s and the infimum over t: ⨅ i ∈ insert x t, update f x s i = s ⊓ ⨅ i ∈ t, f i.

Русский

Пусть x ∈ α, t Finset α, f: α → β, hx: x ∉ t. Тогда инфиминум по insert x t обновления функции равен инфиминуму: ⨅ i ∈ insert x t, update f x s i = s ∧ ⨅ i ∈ t, f i.

LaTeX

$$$$\\displaystyle \\inf_{i \\in \\operatorname{insert}(x,t)} (\\operatorname{update} f x s)(i) = s \\wedge \\inf_{i \\in t} f(i). $$$$

Lean4

theorem iInf_insert_update {x : α} {t : Finset α} (f : α → β) {s : β} (hx : x ∉ t) :
    ⨅ i ∈ insert x t, update f x s i = s ⊓ ⨅ i ∈ t, f i :=
  @iSup_insert_update α βᵒᵈ _ _ _ _ f _ hx

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