bot_eq_one' — Mathlib

English

In a linearly ordered monoid with a bottom element, the bottom element is equal to the unit: ⊥ = 1.

Русский

В линейно упорядоченном моноиде с нулём снизу нижняя граница равна единице: ⊥ = 1.

LaTeX

$$⊥ = 1$$

Lean4

/-- In a linearly ordered monoid, we are happy for `bot_eq_one` to be a `@[simp]` lemma. -/
@[to_additive (attr := simp) /-- In a linearly ordered monoid, we are happy for `bot_eq_zero` to be a `@[simp]` lemma -/
    ]
theorem bot_eq_one' [OrderBot α] : (⊥ : α) = 1 :=
  bot_eq_one

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