const_inj — Mathlib

English

For any nontrivial l, two constant germs are equal if and only if their constants are equal: the germ of a is equal to the germ of b iff a = b.

Русский

При неклонном фильтре l константные жермы a и b равны тогда и только тогда, когда a = b.

LaTeX

$$$ (\\uparrow a : \\mathrm{Germ}(l,\\beta)) = \\uparrow b \\;\\;\\Leftrightarrow \\;\\; a = b $ (при \\mathrm{l.NeBot}).$$$

Lean4

@[simp, norm_cast]
theorem const_inj [NeBot l] {a b : β} : (↑a : Germ l β) = ↑b ↔ a = b :=
  coe_eq.trans const_eventuallyEq

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