finLiftOn — Mathlib

English

Lift a function on the base family to a function on the quotient family via finChoice.

Русский

Поднять функцию с основания до функции на фактор-объектах через finChoice.

LaTeX

$$$\\operatorname{finLiftOn}(q, f, h) = (\\operatorname{finChoice} q).liftOn f h$$$

Lean4

/-- Lift a function on `∀ i, α i` to a function on `∀ i, Quotient (S i)`. -/
def finLiftOn (q : ∀ i, Quotient (S i)) (f : (∀ i, α i) → β) (h : ∀ (a b : ∀ i, α i), (∀ i, a i ≈ b i) → f a = f b) :
    β :=
  (finChoice q).liftOn f h

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