iSup_eq_dif — Mathlib

English

Let p be a proposition with decidable truth, and a : p → α. Then the supremum over h : p of a(h) equals the conditional expression if h is in p, otherwise ⊥.

Русский

Пусть p — пропозиция с разрешимой определённостью, и a : p → α. Тогда ⨆ h : p, a(h) = if h : p then a(h) else ⊥.

LaTeX

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

Lean4

theorem iSup_eq_dif {p : Prop} [Decidable p] (a : p → α) : ⨆ h : p, a h = if h : p then a h else ⊥ := by
  by_cases h : p <;> simp [h]

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