ext — Mathlib

English

Let c and d be concepts of the same polarity relation. If their extents are equal, then c and d are the same concept.

Русский

Пусть c и d — концепты для одной и той же связки. Если их экстенты совпадают, то концепты равны.

LaTeX

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

Lean4

@[ext]
theorem ext (h : c.extent = d.extent) : c = d :=
  by
  obtain ⟨s₁, t₁, rfl, _⟩ := c
  obtain ⟨s₂, t₂, rfl, _⟩ := d
  substs h
  rfl

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