eq_top_iff_isIso — Mathlib

English

For any subpresheaf G, G = ⊤ iff its inclusion morphism G.ι is an isomorphism.

Русский

Для любого подпрешафa G, G = ⊤ тогда и только тогда, когда включение G.ι является изоморфизмом.

LaTeX

$$$G = \\top \\;\\iff\\; IsIso\\, G.\\text{ι}$$$

Lean4

theorem eq_top_iff_isIso : G = ⊤ ↔ IsIso G.ι := by
  constructor
  · rintro rfl
    infer_instance
  · intro H
    ext U x
    apply (iff_of_eq (iff_true _)).mpr
    rw [← IsIso.inv_hom_id_apply (G.ι.app U) x]
    exact ((inv (G.ι.app U)) x).2

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