isCoatom_iff — Mathlib

English

Among top-coatoms, there is equivalence: IsCoatom (u b) ↔ IsCoatom b under suitable assumptions.

Русский

Среди коатомов верхнего уровня существует эквивалентность: IsCoatom(u(b)) ↔ IsCoatom(b) при подходящих предпосылках.

LaTeX

$$$\forall b,\ IsCoatom(u(b)) \iff IsCoatom(b)$$$

Lean4

theorem isCoatom_iff [OrderTop α] [IsCoatomic α] [OrderTop β] {l : α → β} {u : β → α} (gi : GaloisInsertion l u)
    (h_coatom : ∀ a : α, IsCoatom a → u (l a) = a) (b : β) : IsCoatom (u b) ↔ IsCoatom b :=
  by
  refine ⟨fun hb => gi.isCoatom_of_image hb, fun hb => ?_⟩
  obtain ⟨a, ha, hab⟩ :=
    (eq_top_or_exists_le_coatom (u b)).resolve_left fun h =>
      hb.1 <| (gi.gc.u_top ▸ gi.l_u_eq ⊤ : l ⊤ = ⊤) ▸ gi.l_u_eq b ▸ congr_arg l h
  have : l a = b :=
    (hb.le_iff.mp (gi.l_u_eq b ▸ gi.gc.monotone_l hab : b ≤ l a)).resolve_left fun hla =>
      ha.1 (gi.gc.u_top ▸ h_coatom a ha ▸ congr_arg u hla)
  exact this ▸ (h_coatom a ha).symm ▸ ha

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