lt_subset_interior_le — Mathlib

English

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

Русский

Для непрерывных f,g множество {b | f(b) < g(b)} вложено в interior {b | f(b) ≤ g(b)}.

LaTeX

$$$ \\{b \\mid f(b) < g(b)\\} \\subseteq \\operatorname{int}\\{b \\mid f(b) \\le g(b)\\} $$$

Lean4

theorem lt_subset_interior_le (hf : Continuous f) (hg : Continuous g) : {b | f b < g b} ⊆ interior {b | f b ≤ g b} :=
  (interior_maximal fun _ => le_of_lt) <| isOpen_lt hf hg

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