coe_notMemRangeEquiv — Mathlib

English

The forward map of NotMemRangeEquiv(k) is explicitly given by i ↦ i − k.

Русский

Переходная карта NotMemRangeEquiv(k) явно задаётся как i ↦ i − k.

LaTeX

$$$$ \operatorname{coe}(\text{notMemRangeEquiv}(k)) = (\lambda i:\{ n \mid n ∉ \operatorname{range}(k) \}, n \mapsto n - k). $$$$

Lean4

@[simp]
theorem coe_notMemRangeEquiv (k : ℕ) :
    (notMemRangeEquiv k : { n // n ∉ range k } → ℕ) = fun (i : { n // n ∉ range k }) => i - k :=
  rfl

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