map_cast' — Mathlib

English

Casting out of SignType respects composition with functions preserving 0, 1, -1.

Русский

Выведение по SignType сохраняется при композиции с функциями, сохраняющими 0, 1, -1.

LaTeX

$$\forall {α} [Zero α] [One α] [Neg α] {β} [One β] [Neg β] [Zero β] (f : α → β),\forall s : SignType, f s = s$$

Lean4

/-- Casting out of `SignType` respects composition with functions preserving `0, 1, -1`. -/
theorem map_cast' {β : Type*} [One β] [Neg β] [Zero β] (f : α → β) (h₁ : f 1 = 1) (h₂ : f 0 = 0) (h₃ : f (-1) = -1)
    (s : SignType) : f s = s := by cases s <;> simp only [SignType.cast, h₁, h₂, h₃]

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