iInf_coe — Mathlib

English

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

Русский

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

LaTeX

$$$$\\displaystyle \\inf_{x \\in (\\uparrow s)} f(x) = \\inf_{x \\in s} f(x). $$$$

Lean4

theorem iInf_coe [InfSet β] (f : α → β) (s : Finset α) : ⨅ x ∈ (↑s : Set α), f x = ⨅ x ∈ s, f x :=
  rfl

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