iSup_coe — Mathlib

English

For any f: α → β and Finset s, the supremum over the coerced set (↑s : Set α) equals the supremum over s: ⨆ x ∈ (↑s : Set α), f x = ⨆ x ∈ s, f x.

Русский

Для любой f: α → β и конечного множества s верно: ⨆ x ∈ (↑s : Set α), f x = ⨆ x ∈ s, f x.

LaTeX

$$$$\\displaystyle \\big\\langle\\!\\!\\!\\!\\!\\!\\!\\; \\sup_{x \\in (\\uparrow s)} f(x) = \\sup_{x \\in s} f(x) \\!\\!\\!\\!\\!\\!\\!\\;\\rangle.$$$$

Lean4

theorem iSup_coe [SupSet β] (f : α → β) (s : Finset α) : ⨆ x ∈ (↑s : Set α), f x = ⨆ x ∈ s, f x :=
  rfl

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