isAtom_iff' — Mathlib

English

A variant: IsAtom(u(b)) ↔ IsAtom(b) under certain assumptions of a Galois insertion.

Русский

Вариант: IsAtom(u(b)) ↔ IsAtom(b) при определённых предпосылках Galois-подстановки.

LaTeX

$$$\forall b,\ IsAtom(u(b)) \iff IsAtom(b) \;\; (under\; assumptions)$$$

Lean4

theorem isAtom_iff' [OrderBot α] [IsAtomic α] [OrderBot β] {l : α → β} {u : β → α} (gi : GaloisInsertion l u)
    (hbot : u ⊥ = ⊥) (h_atom : ∀ a, IsAtom a → u (l a) = a) (b : β) : IsAtom (u b) ↔ IsAtom b := by
  rw [← gi.isAtom_iff hbot h_atom, gi.l_u_eq]

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