top_apply' — Mathlib

English

For any set s, (⊤) s equals the infimum over all proofs that s = ∅ of 0.

Русский

Для любого s, (⊤) s равно инфимума по всем доказательствам того, что s = ∅, от значения 0.

LaTeX

$$$ (\top : OuterMeasure\ α)\ s = \inf_{p: s = ∅} 0 $$$

Lean4

theorem top_apply' (s : Set α) : (⊤ : OuterMeasure α) s = ⨅ _ : s = ∅, 0 :=
  s.eq_empty_or_nonempty.elim (fun h => by simp [h]) fun h => by simp [h, h.ne_empty]

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