ext — Mathlib

English

Two LowerAdjoint are equal if their underlying functions are equal.

Русский

Два LowerAdjoint равны, если равны их базовые функции.

LaTeX

$$$\\\\forall l_1 l_2 : LowerAdjoint u, \\\\; (l_1 : \\alpha \\to \\beta) = (l_2 : \\alpha \\to \\beta) \\\\Rightarrow l_1 = l_2$$$

Lean4

@[ext]
theorem ext : ∀ l₁ l₂ : LowerAdjoint u, (l₁ : α → β) = (l₂ : α → β) → l₁ = l₂
  | ⟨l₁, _⟩, ⟨l₂, _⟩, h => by congr

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