lift₃_p₁ — Mathlib

English

A three-way lifting relation for a relatively representable morphism expresses that composing the lift with p1 yields x1.

Русский

Трёхкратное поднятие для относительно представимого морфизма выражает, что композиция lift с p1 даёт x1.

LaTeX

$$hf₁.lift₃ f₂ f₃ x₁ x₂ x₃ h₁₂ h₁₃ ∘ p₁ hf₁ f₂ f₃ = x₁$$

Lean4

@[reassoc (attr := simp)]
theorem lift₃_p₁ : hf₁.lift₃ f₂ f₃ x₁ x₂ x₃ h₁₂ h₁₃ ≫ pullback₃.p₁ hf₁ f₂ f₃ = x₁ := by simp [lift₃, pullback₃.p₁]

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