nonempty_frontier_iff — Mathlib

English

For a Preconnected space, (frontier s).Nonempty iff s.Nonempty and s ≠ univ.

Русский

Для предсвязного пространства, frontier s непусто тогда, когда s непусто и s ≠ univ.

LaTeX

$$$[PreconnectedSpace\\;\\alpha] \\; (frontier(s)).Nonempty \\iff s.Nonempty \\land s \\neq univ$$$

Lean4

theorem nonempty_frontier_iff [PreconnectedSpace α] {s : Set α} : (frontier s).Nonempty ↔ s.Nonempty ∧ s ≠ univ := by
  simp only [nonempty_iff_ne_empty, Ne, frontier_eq_empty_iff, not_or]

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