interior — Mathlib

English

The interior of a set s, as an element of Opens, is the pair (interior s, isOpen_interior).

Русский

interior(s) как элемент Opens — это пара (interior s, isOpen_interior).

LaTeX

$$$\mathrm{Opens.interior}(s) = \langle \operatorname{interior}(s), \operatorname{isOpen\_interior}\rangle$$$

Lean4

/-- The interior of a set, as an element of `Opens`. -/
@[simps]
protected def interior (s : Set α) : Opens α :=
  ⟨interior s, isOpen_interior⟩

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