closure_lt_subset_le — Mathlib

English

For continuous f,g, the closure of {b | f(b) < g(b)} is contained in {b | f(b) ≤ g(b)}.

Русский

При непрерывных f,g closure{b | f(b) < g(b)} ⊆ {b | f(b) ≤ g(b)}.

LaTeX

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

Lean4

theorem closure_lt_subset_le [TopologicalSpace β] {f g : β → α} (hf : Continuous f) (hg : Continuous g) :
    closure {b | f b < g b} ⊆ {b | f b ≤ g b} :=
  (closure_minimal fun _ => le_of_lt) <| isClosed_le hf hg

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