English
Given a germ and a function F, lift the germ to a value by applying F to any representative, provided F respects eventual equality.
Русский
Дан зародыш и функция F, поднимаем значение зародыша путём применения F к представителю, если F сохраняет эквивалентность почти везде.
LaTeX
$$$ \mathrm{liftOn}(f, F, hF) = \text{quotient-lift-on } f \; F \; hF$$$
Lean4
/-- Given a germ `f : Germ l β` and a function `F : (α → β) → γ` sending eventually equal functions
to the same value, returns the value `F` takes on functions having germ `f` at `l`. -/
def liftOn {γ : Sort*} (f : Germ l β) (F : (α → β) → γ) (hF : (l.EventuallyEq ⇒ (· = ·)) F F) : γ :=
Quotient.liftOn' f F hF
