frontier_lt_subset_eq — Mathlib

English

For continuous f,g, frontier {b | f(b) < g(b)} ⊆ {b | f(b) = g(b)}.

Русский

Для непрерывных f,g граница {b | f(b) < g(b)} ⊆ {b | f(b) = g(b)}.

LaTeX

$$$ \\text{frontier} \\{b \\mid f(b) < g(b)\\} \\subseteq \\{b \\mid f(b)=g(b)\\}$$$

Lean4

theorem frontier_lt_subset_eq (hf : Continuous f) (hg : Continuous g) : frontier {b | f b < g b} ⊆ {b | f b = g b} := by
  simpa only [← not_lt, ← compl_setOf, frontier_compl, eq_comm] using frontier_le_subset_eq hg hf

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