iInf_eq_if — Mathlib

English

Let p be a proposition with decidable truth and a : p → α. Then the infimum over h : p of a(h) equals if h : p then a(h) else ⊤.

Русский

Пусть p — пропозиция с разрешимой判, и a : p → α. Тогда ⨅ h : p, a(h) = if h : p then a(h) else ⊤.

LaTeX

$$$$\bigwedge_{h : p} a(h) = \text{if } h : p \text{ then } a(h) \text{ else } \top.$$$$

Lean4

theorem iInf_eq_if {p : Prop} [Decidable p] (a : α) : ⨅ _ : p, a = if p then a else ⊤ :=
  iInf_eq_dif fun _ => a

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