isAtom_of_u_bot — Mathlib

English

In a Galois insertion with bottom, if u(⊥)=⊥ and u(b) is an atom, then b is an atom.

Русский

В Galois-подстановке с нижним предикатом, если u(⊥)=⊥ и u(b) атом, то b атом.

LaTeX

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

Lean4

theorem isAtom_of_u_bot [OrderBot α] [OrderBot β] {l : α → β} {u : β → α} (gi : GaloisInsertion l u) (hbot : u ⊥ = ⊥)
    {b : β} (hb : IsAtom (u b)) : IsAtom b :=
  OrderEmbedding.isAtom_of_map_bot_of_image ⟨⟨u, gi.u_injective⟩, @GaloisInsertion.u_le_u_iff _ _ _ _ _ _ gi⟩ hbot hb

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