isClosed — Mathlib

English

If A is closed and B is exposed relative to A, then B is closed (under appropriate topological assumptions).

Русский

Если A замкнутое и B экспонировано относительно A, то B замкнутое (при подходящих топологических условиях).

LaTeX

$$$$ IsExposed\ 𝕜\ A\ B \to IsClosed\ A \to IsClosed\ B. $$$$

Lean4

protected theorem isClosed [OrderClosedTopology 𝕜] {A B : Set E} (hAB : IsExposed 𝕜 A B) (hA : IsClosed A) :
    IsClosed B := by
  obtain rfl | hB := B.eq_empty_or_nonempty
  · simp
  obtain ⟨l, a, rfl⟩ := hAB.eq_inter_halfSpace' hB
  exact hA.isClosed_le continuousOn_const l.continuous.continuousOn

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