iInf_option — Mathlib

English

For a function f: Option β → α, the infimum over all options equals the minimum of the value at none and the infimum over all some values: ⨅ o, f o = f none ⊓ ⨅ b, f (Some b).

Русский

Для функции f: Option β → α инфимум по всем Option равен минимуму значения в none и инфимума по всем some b: ⨅ o, f o = f none ⊓ ⨅ b, f (Some b).

LaTeX

$$$\\displaystyle \\big\\wedge_{o} f(o) = f(\\text{none}) \\;\\sqcap\\; \\big\\wedge_{b} f(\\text{Some } b)$$$

Lean4

theorem iInf_option (f : Option β → α) : ⨅ o, f o = f none ⊓ ⨅ b, f (Option.some b) :=
  @iSup_option αᵒᵈ _ _ _

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