coe_eq — Mathlib

English

Coercion into Germ l β identifies functions with respect to eventual equality: f equals g in Germ iff f and g are eventually equal along l.

Русский

Вмещение в зародыш lβ идентифицирует функции по эквивалентности почти везде: f = g в зародышe тогда и только тогда, когда f ≈ g по l.

LaTeX

$$$ (f : \mathrm{Germ}(l, \beta)) = g \iff f =^{\!\!}_{l} g $$$

Lean4

@[simp, norm_cast]
theorem coe_eq : (f : Germ l β) = g ↔ f =ᶠ[l] g :=
  Quotient.eq''

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