ofCauchy_sup — Mathlib

English

The completion map distributes sup over mk: mk f ≤ mk g corresponds to f ≤ g and the join behaves with mk.

Русский

Отображение mk распределяет операцию объединения по отношению к mk: mk f ⊔ mk g = mk (f ⊔ g).

LaTeX

$$$\mathrm{mk}(f \sqcup g) = \mathrm{mk}(f) \sqcup \mathrm{mk}(g)$$$

Lean4

theorem ofCauchy_sup (a b) : (⟨⟦a ⊔ b⟧⟩ : ℝ) = ⟨⟦a⟧⟩ ⊔ ⟨⟦b⟧⟩ :=
  show _ = sup _ _ by
    rw [sup_def]
    rfl

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