instOrderBot — Mathlib

English

The space of finite-support functions Π₀ i, α_i has a bottom element given by the zero function, and this bottom is below every element of the space.

Русский

Множество DFinsupp ⟨i⟩ α_i имеет нижнюю границу, заданную нулевой функцией; она лежит ниже всякого элемента пространства.

LaTeX

$$∃ bot,bot := 0 ∧ ∀ f, bot ≤ f$$

Lean4

instance : OrderBot (Π₀ i, α i) where
  bot := 0
  bot_le := by simp only [le_def, coe_zero, Pi.zero_apply, imp_true_iff, zero_le]

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