Icc01 — Mathlib

English

The interval [0,1] is compact and has nonempty interior in the standard real line.

Русский

Интервал [0,1] компактен и имеет непустое interior в стандартной вещественной оси.

LaTeX

$$$[0,1] \text{ is compact and } \mathrm{Int}([0,1]) \neq \emptyset$$$

Lean4

/-- The interval `[0,1]` as a compact set with non-empty interior. -/
def Icc01 : PositiveCompacts ℝ where
  carrier := Icc 0 1
  isCompact' := isCompact_Icc
  interior_nonempty' := by simp_rw [interior_Icc, nonempty_Ioo, zero_lt_one]

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