interior — Mathlib

English

Repeats that the interior of an OrdConnected set is OrdConnected.

Русский

Повторение: Interior OrdConnected сохраняет OrdConnected.

LaTeX

$$$\\text{If } s.OrdConnected, \\mathrm{int}\\;s \\text{ is OrdConnected}$$$

Lean4

protected theorem interior (h : s.OrdConnected) : (interior s).OrdConnected :=
  by
  rw [← h.upperClosure_inter_lowerClosure, interior_inter]
  exact (upperClosure s).upper.interior.ordConnected.inter (lowerClosure s).lower.interior.ordConnected

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