ext' — Mathlib

English

Two pretrivializations are equal if their underlying partial equivalences and base sets agree.

Русский

Две предтривализации равны, если их базовые частичные эквивалентности и базовые множества совпадают.

LaTeX

$$$e=e'\ \text{ если }\ e.toPartialEquiv = e'.toPartialEquiv\ \land\ e.baseSet = e'.baseSet$$$

Lean4

@[ext]
theorem ext' (e e' : Pretrivialization F proj) (h₁ : e.toPartialEquiv = e'.toPartialEquiv)
    (h₂ : e.baseSet = e'.baseSet) : e = e' := by cases e; cases e';
  congr
    -- TODO: move `ext` here?

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