exists_covBy_le_of_lt — Mathlib

English

In a strongly atomic poset, if a < b, there exists x with a ⋖ x and x ≤ b.

Русский

В сильно атомарном частично упорядоченном множестве, если a < b, существует x such that a ⋖ x и x ≤ b.

LaTeX

$$$ [IsStronglyAtomic α] (a < b) \rightarrow \exists x, a \,⋖\, x \land x \le b $$$

Lean4

theorem exists_covBy_le_of_lt [IsStronglyAtomic α] (h : a < b) : ∃ x, a ⋖ x ∧ x ≤ b :=
  IsStronglyAtomic.exists_covBy_le_of_lt a b h

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