ext' — Mathlib

English

Let c and d be concepts. If their intents are equal, then c equals d.

Русский

Пусть два концепта имеют одинаковые интенты; тогда они равны.

LaTeX

$$$\forall \alpha \forall \beta \forall r:\alpha \to \beta \to \mathrm{Prop}, \forall c,d : \mathrm{Concept}\,\alpha\,\beta\,r,\; c.intent = d.intent \rightarrow c = d$$$

Lean4

theorem ext' (h : c.intent = d.intent) : c = d :=
  by
  obtain ⟨s₁, t₁, _, rfl⟩ := c
  obtain ⟨s₂, t₂, _, rfl⟩ := d
  substs h
  rfl

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