orderBot — Mathlib

English

There is a bottom element in OuterMeasure α, namely the zero outer measure, which is less than or equal to every outer measure.

Русский

Существует нижний элемент в OuterMeasure α, равный нулевой внешней мере, который не превосходит любую другую внешнюю меру.

LaTeX

$$$\text{OrderBot }(OuterMeasure\, \alpha)\;:\; \mathrm{bot} = 0$, and $0 \le m$ for all $m$.$$

Lean4

instance orderBot : OrderBot (OuterMeasure α) :=
  { bot := 0, bot_le := fun a s => by simp only [coe_zero, Pi.zero_apply, zero_le] }

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