iInf_option_elim — Mathlib

English

A dual form of iSup_option_elim: for a and f as above, the infimum over o : Option β of o.elim a f equals a ∧ inf_{b} f b.

Русский

Дуальная форма iSup_option_elim: для a и f как выше инфимуум по o : Option β от o.elim a f равен a ∧ inf_{b} f(b).

LaTeX

$$$\\displaystyle \\big\\wedge_{o:\\mathrm{Option}\\,\\beta} (o.elim\\ a\\ f) = a \\;\\sqcap\\; \\big\\wedge_{b} f(b)$$$

Lean4

/-- A version of `iInf_option` useful for rewriting right-to-left. -/
theorem iInf_option_elim (a : α) (f : β → α) : ⨅ o : Option β, o.elim a f = a ⊓ ⨅ b, f b :=
  @iSup_option_elim αᵒᵈ _ _ _ _

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