iSup_insert — Mathlib

English

For a ∈ α, Finset s and t: α → β, the supremum over insert a s satisfies: ⨆ x ∈ insert a s, t x = t a ⊔ ⨆ x ∈ s, t x.

Русский

Для элемента a, множества s и функции t: α → β верно: ⨆ x ∈ insert a s, t x = t a ⊔ ⨆ x ∈ s, t x.

LaTeX

$$$$\\displaystyle \\sup_{x \\in \\operatorname{insert}(a,s)} t(x) = t(a) \\vee \\sup_{x \\in s} t(x). $$$$

Lean4

theorem iSup_insert (a : α) (s : Finset α) (t : α → β) : ⨆ x ∈ insert a s, t x = t a ⊔ ⨆ x ∈ s, t x :=
  by
  rw [insert_eq]
  simp only [iSup_union, Finset.iSup_singleton]

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