ext' — Mathlib

English

Continuing the extensionality principle for another alignment of two trivializations.

Русский

Продолжаем принцип экстенсиональности для другой пары тривиализаций.

LaTeX

$$$e.toOpenPartialHomeomorph = e'.toOpenPartialHomeomorph\land\; e.baseSet = e'.baseSet\Rightarrow e = e'$$$

Lean4

@[ext]
theorem ext' (e e' : Trivialization F proj) (h₁ : e.toOpenPartialHomeomorph = e'.toOpenPartialHomeomorph)
    (h₂ : e.baseSet = e'.baseSet) : e = e' := by cases e; cases e'; congr

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