subtypeOrderIso — Mathlib

English

Equality of the coercion map with the dual composition is definitional.

Русский

Сохранение определения эквивалентности отображений через дуальность.

LaTeX

$$$(WithBot.toDualTopEquiv) = (toDual \\circ WithBot.ofDual)$$$

Lean4

/-- Any `OrderBot` is equivalent to `WithBot` of the subtype excluding `⊥`.

See also `Equiv.optionSubtypeNe`. -/
def subtypeOrderIso [PartialOrder α] [OrderBot α] [DecidablePred (· = (⊥ : α))] : WithBot { a : α // a ≠ ⊥ } ≃o α :=
  (WithTop.subtypeOrderIso (α := αᵒᵈ)).dual

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