isClosed_le — Mathlib

English

For continuous maps f,g: β → α between spaces, the set {b | f(b) ≤ g(b)} is closed.

Русский

Для непрерывных отображений f,g: β → α множество {b | f(b) ≤ g(b)} замкнуто.

LaTeX

$$$\text{IsClosed} \{ b \mid f(b) \le g(b) \}$$$

Lean4

theorem isClosed_le [TopologicalSpace β] {f g : β → α} (hf : Continuous f) (hg : Continuous g) :
    IsClosed {b | f b ≤ g b} :=
  continuous_iff_isClosed.mp (hf.prodMk hg) _ isClosed_le_prod

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