isAtom_iff — Mathlib

English

For any a in Set.Ici, the element b is an atom exactly when it covers a, i.e., a ⋖ b.

Русский

Для любого b ∈ Set.Ici(a) элемент b является атомом тогда и только тогда, когда он покрывает a, то есть a ⋖ b.

LaTeX

$$$ \\forall {b : Set.Ici(a)}, \\mathrm{IsAtom}(b) \\leftrightarrow a \\lessdot b.$$

Lean4

@[simp]
theorem isAtom_iff {b : Set.Ici a} : IsAtom b ↔ a ⋖ b :=
  by
  rw [← bot_covBy_iff]
  refine (Set.OrdConnected.apply_covBy_apply_iff (OrderEmbedding.subtype fun c => a ≤ c) ?_).symm
  simpa only [OrderEmbedding.coe_subtype, Subtype.range_coe_subtype] using Set.ordConnected_Ici

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