const_inj — Mathlib

English

Two constant CauSeqs are equal iff the underlying constants are equal: (const abv x) = (const abv y) iff x = y.

Русский

Две константные CauSeq равны тогда и только тогда, когда константы равны: (const abv x) = (const abv y) ⇔ x = y.

LaTeX

$$$(\\text{CauSeq.const abv x}) = (\\text{CauSeq.const abv y}) \\iff x = y$$$

Lean4

theorem const_inj {x y : β} : (const x : CauSeq β abv) = const y ↔ x = y :=
  ⟨fun h => congr_arg (fun f : CauSeq β abv => (f : ℕ → β) 0) h, congr_arg _⟩

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