bit_cases_on_injective — Mathlib

English

The map H ↦ (n ↦ bitCasesOn n H) is injective: if bitCasesOn n H1 = bitCasesOn n H2 for all n, then H1 = H2.

Русский

Отображение H ↦ (n ↦ bitCasesOn n H) иньективно: если bitCasesOn n H1 = bitCasesOn n H2 для всех n, то H1 = H2.

LaTeX

$$$$ \text{Injective}(H) :\; \!\; \forall H_1,H_2,\; (\forall n, \text{bitCasesOn}(n,H_1) = \text{bitCasesOn}(n,H_2)) \Rightarrow H_1 = H_2. $$$$

Lean4

theorem bit_cases_on_injective {motive : ℕ → Sort u} :
    Function.Injective fun H : ∀ b n, motive (bit b n) => fun n => bitCasesOn n H :=
  by
  intro H₁ H₂ h
  ext b n
  simpa only [bitCasesOn_bit] using congr_fun h (bit b n)

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