hasse_preconnected_of_pred — Mathlib

English

For a linear order with PredOrder and IsPredArchimedean, the Hasse diagram is preconnected.

Русский

При линейном порядке с PredOrder и IsPredArchimedean диаграмма Хассе предсоединена.

LaTeX

$$$\forall \alpha, [PredOrder(\alpha)] [IsPredArchimedean(\alpha)] \Rightarrow (hasse \alpha).Preconnected$$$

Lean4

theorem hasse_preconnected_of_pred [PredOrder α] [IsPredArchimedean α] : (hasse α).Preconnected := fun a b =>
  by
  rw [reachable_iff_reflTransGen, ← reflTransGen_swap]
  exact
    reflTransGen_of_pred _ (fun c hc => Or.inl <| pred_covBy_of_not_isMin hc.1.not_isMin) fun c hc =>
      Or.inr <| pred_covBy_of_not_isMin hc.1.not_isMin

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