English
LiftRel r lifts a relation on β, γ to germs by requiring r to hold pointwise almost everywhere.
Русский
LiftRel r поднимает отношение r на жермы β и γ, требуя, чтобы выполнялось по точкам почти повсеместно.
LaTeX
$$$ \\mathrm{LiftRel}(r) (f : \\mathrm{Germ}(l,\\beta)) (g : \\mathrm{Germ}(l,\\gamma)) \\;:=\\; \\forall^\\infty x \\in l, r (f(x)) (g(x)) $$$
Lean4
/-- Lift a relation `r : β → γ → Prop` to `Germ l β → Germ l γ → Prop`. -/
def LiftRel (r : β → γ → Prop) (f : Germ l β) (g : Germ l γ) : Prop :=
Quotient.liftOn₂' f g (fun f g => ∀ᶠ x in l, r (f x) (g x)) fun _f _g _f' _g' Hf Hg =>
propext <| eventually_congr <| Hg.mp <| Hf.mono fun _x hf hg => hf ▸ hg ▸ Iff.rfl
