ext — Mathlib

English

Opens α is determined by its carrier: if two opens have the same underlying set, they are equal.

Русский

Открытые множества задаются по их карриеру: если два открытых множества имеют одно и то же основание, то они равны.

LaTeX

$$$\forall {U,V : \mathrm{Opens}(\alpha)}, (U : Set α) = (V : Set α) \Rightarrow U = V.$$$

Lean4

@[ext] -- TODO: replace with `∀ x, x ∈ U ↔ x ∈ V`?

theorem ext {U V : Opens α} (h : (U : Set α) = V) : U = V :=
  SetLike.coe_injective h

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