isIso_iff — Mathlib

English

An arrow in a pullback is an isomorphism if and only if both its fst and snd components are isomorphisms.

Русский

Стрелка в pullback является изоморфизмом тогда и только тогда, когда обе её компоненты fst и snd являются изоморфизмами.

LaTeX

$$$ IsIso\ f \iff (IsIso\ f.fst \land IsIso\ f.snd)$$$

Lean4

theorem isIso_iff {x y : F ⊡ G} (f : x ⟶ y) : IsIso f ↔ (IsIso f.fst ∧ IsIso f.snd)
    where
  mp h := ⟨inferInstance, inferInstance⟩
  mpr
    | ⟨h₁, h₂⟩ => ⟨⟨inv f.fst, inv f.snd, by cat_disch⟩, by cat_disch⟩

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