coe_wcovBy_coe — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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