not_isPredPrelimit_iff_exists_covBy

English

In a linear order, a is not a predecessor-prelimit iff there exists b with a ⋖ b (a is covered by b).

Русский

В линейном порядке a не является пред-предлимитом тогда и только тогда, когда существует b such that a ⋖ b (a покрыт b).

LaTeX

$$$\not\IsPredPrelimit(a) \iff \exists b, \ a \triangleleft b$$$

Lean4

theorem not_isPredPrelimit_iff_exists_covBy (a : α) : ¬IsPredPrelimit a ↔ ∃ b, a ⋖ b := by simp [IsPredPrelimit]

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