ωSup_eq_some — Mathlib

English

A simp-friendly variant: if a ∈ c then Part.ωSup c = Part.some a.

Русский

Упрощённо: если a ∈ c, то Part.ωSup c = Part.some a.

LaTeX

$$$$ \text{Part.ωSup } c = \text{Part.some } a \quad \text{ when } a \in c. $$$$

Lean4

theorem ωSup_eq_some {c : Chain (Part α)} {a : α} (h : some a ∈ c) : Part.ωSup c = some a :=
  have : ∃ a, some a ∈ c := ⟨a, h⟩
  have a' : some (Classical.choose this) ∈ c := Classical.choose_spec this
  calc
    Part.ωSup c = some (Classical.choose this) := dif_pos this
    _ = some a := congr_arg _ (eq_of_chain a' h)

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