mem_domain_sSup_iff — Mathlib

English

For nonempty c and directed hc, x ∈ dom(sSup c) iff there exists f ∈ c with x ∈ dom f.

Русский

Для непустого c и направленного hc верно: x ∈ дом(c) суп if и только если существует f∈c с x ∈ dom f.

LaTeX

$$$$ x \\in \\operatorname{dom}(\\mathrm{sSup}(c)) \\iff \\exists f\\in c, x\\in \\operatorname{dom}(f). $$$$

Lean4

theorem mem_domain_sSup_iff {c : Set (E →ₗ.[R] F)} (hnonempty : c.Nonempty) (hc : DirectedOn (· ≤ ·) c) {x : E} :
    x ∈ (LinearPMap.sSup c hc).domain ↔ ∃ f ∈ c, x ∈ f.domain :=
  by
  rw [domain_sSup,
    Submodule.mem_sSup_of_directed (hnonempty.image _) (DirectedOn.mono_comp LinearPMap.domain_mono.monotone hc)]
  simp

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