instFunLike — Mathlib

English

A splitting is a function-like object: it determines a map from G to E, and two splittings are equal if and only if their underlying functions coincide.

Русский

Разбиение является функтообразным объектом: оно задаёт отображение от G в E, и два разбиения равны тогда и только тогда, когда их основанные функции совпадают.

LaTeX

$$$ s_1.toFun = s_2.toFun \\Rightarrow s_1 = s_2 \\quad\\text{(extensionality of the splitting as a function)}$$$

Lean4

@[to_additive]
instance : FunLike S.Splitting G E where
  coe s := s.toFun
  coe_injective' := by
    intro ⟨_, _⟩ ⟨_, _⟩ h
    congr
    exact DFunLike.coe_injective h

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