English
Let α be a locally finite preorder. Then for any a < b in α there exists an element x with a < x ≤ b and a is covered by x (i.e., a ⋖ x). In words, every interval [a,b] with a < b contains an element that immediately succeeds a.
Русский
Пусть α – локально конечный предпорядок. Тогда для любых a < b в α существует элемент x such that a < x ≤ b и a покрывается x (то есть a ⋖ x). Иными словами, каждый интервал [a, b] с a < b содержит элемент, являющийся непосредственным преемником a.
LaTeX
$$$\forall a,b\,(a < b \rightarrow \exists x\ (a < x \land x \le b \land \nexists y\ (a < y \land y < x))).$$$
Lean4
instance : IsStronglyAtomic α where
exists_covBy_le_of_lt a b
hab :=
by
obtain ⟨x, hx, hxmin⟩ :=
(LocallyFiniteOrder.finsetIoc a b).exists_minimal ⟨b, by simpa [LocallyFiniteOrder.finset_mem_Ioc]⟩
simp only [LocallyFiniteOrder.finset_mem_Ioc] at hx hxmin
exact ⟨x, ⟨hx.1, fun c hac hcx ↦ hcx.not_ge <| hxmin ⟨hac, hcx.le.trans hx.2⟩ hcx.le⟩, hx.2⟩
