English
Let x ∈ α, t Finset α, f: α → β, and s ∈ β with hx: x ∉ t. Then the supremum over insert x t of Function.update f x s equals the maximum of s and the supremum over t: ⨆ i ∈ insert x t, (update f x s i) = s ⊔ ⨆ i ∈ t, f i.
Русский
Пусть x ∈ α, t = Finset α, f: α → β, s ∈ β и hx: x ∉ t. Тогда ⨆ i ∈ insert x t, update f x s i = max{s, ⨆ i ∈ t, f i}.
LaTeX
$$$$\\displaystyle \\sup_{i \\in \\operatorname{insert}(x,t)} (\\operatorname{update} f x s)(i) = s \\;\vee\\; \\sup_{i \\in t} f(i). $$$$
Lean4
theorem iSup_insert_update {x : α} {t : Finset α} (f : α → β) {s : β} (hx : x ∉ t) :
⨆ i ∈ insert x t, Function.update f x s i = s ⊔ ⨆ i ∈ t, f i :=
by
simp only [Finset.iSup_insert, update_self]
rcongr (i hi); apply update_of_ne; rintro rfl; exact hx hi
