orderIsoPUnitSumLex_bot — Mathlib

English

The bottom element maps to the left injection of PUnit under the isomorphism: orderIsoPUnitSumLex.bot = toLex (inl PUnit.unit).

Русский

Нижний элемент переходит под изоморфизм к левой вставке PUnit: orderIsoPUnitSumLex.bot = toLex (inl PUnit.unit).

LaTeX

$$$\\text{orderIsoPUnitSumLex.bot} = \\mathrm{toLex}(\\mathrm{inl}(\\mathrm{PUnit.unit}))$$$

Lean4

@[simp]
theorem orderIsoPUnitSumLex_bot : @orderIsoPUnitSumLex α _ ⊥ = toLex (inl PUnit.unit) :=
  rfl

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