lift₂ — Mathlib

English

For x ∈ X and y ∈ Y, lift₂ f hf (mk x) (mk y) = f x y.

Русский

Для x ∈ X и y ∈ Y имеем lift₂ f hf (mk x) (mk y) = f x y.

LaTeX

$$lift₂ f hf (mk x) (mk y) = f x y$$

Lean4

/-- Lift a map `f : X → Y → α` such that `Inseparable a b → Inseparable c d → f a c = f b d` to a
map `SeparationQuotient X → SeparationQuotient Y → α`. -/
def lift₂ (f : X → Y → α) (hf : ∀ a b c d, (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d) :
    SeparationQuotient X → SeparationQuotient Y → α := fun x y => Quotient.liftOn₂' x y f hf

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