of_wellFounded_lt — Mathlib

English

If the strict order < is well-founded, then α is strongly atomic.

Русский

Если отношение < на α является хорошо основанным, то α сильно атомарна.

LaTeX

$$$\\mathrm{WellFounded}((<)) \\Rightarrow \\mathrm{IsStronglyAtomic}(\\alpha)$$$

Lean4

theorem of_wellFounded_lt (h : WellFounded ((· < ·) : α → α → Prop)) : IsStronglyAtomic α where
  exists_covBy_le_of_lt a b
    hab := by
    refine ⟨WellFounded.min h (Set.Ioc a b) ⟨b, hab, rfl.le⟩, ?_⟩
    have hmem := (WellFounded.min_mem h (Set.Ioc a b) ⟨b, hab, rfl.le⟩)
    exact
      ⟨⟨hmem.1, fun c hac hlt ↦ WellFounded.not_lt_min h (Set.Ioc a b) ⟨b, hab, rfl.le⟩ ⟨hac, hlt.le.trans hmem.2⟩ hlt⟩,
        hmem.2⟩

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