isAtom_iff — Mathlib

English

Under a Galois insertion with bottom, and a suitable atom-preservation condition, IsAtom(l(a)) is equivalent to IsAtom(a) for all a.

Русский

При условии сосохранения атомности, IsAtom(l(a)) эквивалентно IsAtom(a).

LaTeX

$$$\forall a, \text{IsAtom}(l(a)) \iff \text{IsAtom}(a) \;\; (\text{under suitable conditions})$$$

Lean4

theorem isAtom_iff [OrderBot α] [IsAtomic α] [OrderBot β] {l : α → β} {u : β → α} (gi : GaloisInsertion l u)
    (hbot : u ⊥ = ⊥) (h_atom : ∀ a, IsAtom a → u (l a) = a) (a : α) : IsAtom (l a) ↔ IsAtom a :=
  by
  refine ⟨fun hla => ?_, fun ha => gi.isAtom_of_u_bot hbot ((h_atom a ha).symm ▸ ha)⟩
  obtain ⟨a', ha', hab'⟩ := (eq_bot_or_exists_atom_le (u (l a))).resolve_left (hbot ▸ fun h => hla.1 (gi.u_injective h))
  have :=
    (hla.le_iff.mp <| (gi.l_u_eq (l a) ▸ gi.gc.monotone_l hab' : l a' ≤ l a)).resolve_left fun h =>
      ha'.1 (hbot ▸ h_atom a' ha' ▸ congr_arg u h)
  have haa' : a = a' :=
    (ha'.le_iff.mp <| (gi.gc.le_u_l a).trans_eq (h_atom a' ha' ▸ congr_arg u this.symm)).resolve_left
      (mt (congr_arg l) (gi.gc.l_bot.symm ▸ hla.1))
  exact haa'.symm ▸ ha'

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