closure_le_eq — Mathlib

English

If f,g are continuous, then the closure of {b | f(b) ≤ g(b)} equals {b | f(b) ≤ g(b)}.

Русский

Если f и g непрерывны, замыкание множества {b | f(b) ≤ g(b)} совпадает с этим множеством.

LaTeX

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

Lean4

@[simp]
theorem closure_le_eq [TopologicalSpace β] {f g : β → α} (hf : Continuous f) (hg : Continuous g) :
    closure {b | f b ≤ g b} = {b | f b ≤ g b} :=
  (isClosed_le hf hg).closure_eq

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