liftRel_coe — Mathlib

English

Raising a relation to germs via coe: LiftRel r (f : Germ l β) g is equivalent to the pointwise relation.

Русский

Поднятие отношения к жермам по конвертации: LiftRel r (f : Germ l β) g эквивалентно точечному отношению.

LaTeX

$$$ \\mathrm{LiftRel} r (\\mathrm{Germ.ofFun} f) (\\mathrm{Germ.ofFun} g) \\iff \\forall^\\infty x \\in l, r (f x) (g x) $$$

Lean4

@[simp]
theorem liftRel_coe {r : β → γ → Prop} {f : α → β} {g : α → γ} :
    LiftRel r (f : Germ l β) g ↔ ∀ᶠ x in l, r (f x) (g x) :=
  Iff.rfl

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