domain_sSup — Mathlib

English

The domain of sSup(c) equals the supremum of the images of the domains under c.

Русский

Область определения sSup(c) равна верхушке образов доменов под действием c.

LaTeX

$$$$ \\operatorname{dom}(\\mathrm{sSup}(c)) = \\mathrm{sSup}(\\operatorname{domain}''c). $$$$

Lean4

theorem domain_sSup {c : Set (E →ₗ.[R] F)} (hc : DirectedOn (· ≤ ·) c) :
    (LinearPMap.sSup c hc).domain = sSup (LinearPMap.domain '' c) :=
  rfl

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