ciSup_or' — Mathlib

English

For p and q propositions and a function f on p ∨ q, the supremum over p ∨ q equals the supremum over p and over q joined appropriately.

Русский

Для двух булевых условий p, q и функции f на p ∨ q, верхняя грань над объединением равна объединению верхних граней над p и над q.

LaTeX

$$$ \\sup_{h : p \\lor q} f(h) = \\sup_{h : p} f(\\mathrm{inl}\, h) \\; \\vee \\; \\sup_{h : q} f(\\mathrm{inr}\, h) $$$

Lean4

theorem ciSup_or' (p q : Prop) (f : p ∨ q → α) : ⨆ (h : p ∨ q), f h = (⨆ h : p, f (.inl h)) ⊔ ⨆ h : q, f (.inr h) := by
  by_cases hp : p <;> by_cases hq : q <;> simp [hp, hq]

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