pullbackMk_surjective — Mathlib

English

Every element of the pullback can be written as a pullbackMk of some x1 ∈ X1, x2 ∈ X2 and a compatibility h: f1(x1) = f2(x2).

Русский

Любой элемент прообраза можно записать как pullbackMk f1 f2 x1 x2 h с некоторыми x1∈X1, x2∈X2 и совместимостью h: f1(x1)=f2(x2).

LaTeX

$$$\\forall x \\in ToType(pullback f_1 f_2),\\; \\exists x_1 \\in ToType X_1, \\exists x_2 \\in ToType X_2, \\exists h: f_1 x_1 = f_2 x_2,\\\\ x = pullbackMk\ $f_1,f_2$ x_1 x_2 h$$$

Lean4

theorem pullbackMk_surjective (x : ToType (pullback f₁ f₂)) :
    ∃ (x₁ : ToType X₁) (x₂ : ToType X₂) (h : f₁ x₁ = f₂ x₂), x = pullbackMk f₁ f₂ x₁ x₂ h :=
  by
  obtain ⟨⟨⟨x₁, x₂⟩, h⟩, rfl⟩ := (pullbackEquiv f₁ f₂).symm.surjective x
  exact ⟨x₁, x₂, h, rfl⟩

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