sup — Mathlib

English

If f and g are quasiconvex on S, then their pointwise supremum h = f ⊔ g is quasiconvex on S.

Русский

Если f и g на S квазиконвексны, то их точечное объединение h = f ⊔ g тоже квазиконвексно на S.

LaTeX

$$$QuasiconvexOn\ 𝕜\ s\ f \rightarrow QuasiconvexOn\ 𝕜\ s\ g \rightarrow QuasiconvexOn\ 𝕜\ s\ (f \⊔\ g)$$$

Lean4

theorem sup [SemilatticeSup β] (hf : QuasiconvexOn 𝕜 s f) (hg : QuasiconvexOn 𝕜 s g) : QuasiconvexOn 𝕜 s (f ⊔ g) :=
  by
  intro r
  simp_rw [Pi.sup_def, sup_le_iff, Set.sep_and]
  exact (hf r).inter (hg r)

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