coe_covBy_coe — Mathlib

English

CovBy is preserved under the embedding: CovBy (WithTop.some a) (WithTop.some b) iff CovBy a b.

Русский

CovBy сохраняется под вложением: CovBy (WithTop.some a) (WithTop.some b) эквивалентно CovBy a b.

LaTeX

$$$ CovBy (WithTop.some\ a) (WithTop.some\ b) \\iff CovBy\ a\ b $$$

Lean4

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

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