isAtom_of_map_bot_of_image — Mathlib

English

An order-embedding that preserves bottom reflects atoms: if f⊥=⊥ and f(b) is an atom, then b is an atom.

Русский

Условие сохранения нуля и сохранение нижнего предела эмбеддинга отражает атомность: если f⊥=⊥ и f(b) атом, то b атом.

LaTeX

$$$\forall b,\ f\bot = \bot \land \text{IsAtom}(f(b)) \Rightarrow \text{IsAtom}(b)$$$

Lean4

theorem isAtom_of_map_bot_of_image [OrderBot α] [OrderBot β] (f : β ↪o α) (hbot : f ⊥ = ⊥) {b : β} (hb : IsAtom (f b)) :
    IsAtom b := by
  simp only [← bot_covBy_iff] at hb ⊢
  exact CovBy.of_image f (hbot.symm ▸ hb)

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