coe_wcovBy_coe — Mathlib

English

Embedding into WithBot preserves the WCovBy relation: (a : WithBot α) ⩿ b iff a ⩿ b.

Русский

Встраивание в WithBot сохраняет WCovBy: (a : WithBot α) ⩿ b эквивалентно a ⩿ b.

LaTeX

$$$ (a : WithBot α) ⩿ b \\iff a ⩿ b $$$

Lean4

@[simp, norm_cast]
theorem coe_wcovBy_coe : (a : WithBot α) ⩿ b ↔ a ⩿ b :=
  Set.OrdConnected.apply_wcovBy_apply_iff WithBot.coeOrderHom <| by simp [WithBot.range_coe, ordConnected_Ioi]

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