t_inv — Mathlib

English

In the MkCore construction, the composition of the transition maps t_{i j} and t_{j i} is the identity on the overlap V_{j i}.

Русский

В конструирование MkCore композиция переходных отображений t_{i j} и t_{j i} есть тождественное отображение на пересечении V_{j i}.

LaTeX

$$$(t_{i j} \\circ t_{j i}) = \\mathrm{id}_{V_{j i}}$$$

Lean4

theorem t_inv (h : MkCore) (i j : h.J) (x : h.V j i) : h.t i j ((h.t j i) x) = x :=
  by
  have := h.cocycle j i j x ?_
  · rw [h.t_id] at this
    · convert Subtype.eq this
  rw [h.V_id]
  trivial

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