iInf_option_toFinset — Mathlib

English

For an Option α o and f: α → β, the infimum over o.toFinset equals the infimum over o: ⨅ x ∈ o.toFinset, f x = ⨅ x ∈ o, f x.

Русский

Для опции o и функции f: α → β верно: ⨅ x ∈ o.toFinset, f x = ⨅ x ∈ o, f x.

LaTeX

$$$$\\displaystyle \\inf_{x \\in o^{\\mathrm{toFinset}}} f(x) = \\inf_{x \\in o} f(x). $$$$

Lean4

theorem iInf_option_toFinset (o : Option α) (f : α → β) : ⨅ x ∈ o.toFinset, f x = ⨅ x ∈ o, f x :=
  @iSup_option_toFinset _ βᵒᵈ _ _ _

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