instFunLikeNatSet — Mathlib

English

A compact exhaustion can be viewed as a function from natural numbers to subsets of X, sending n to the nth compact subset K_n; this view provides a convenient functional representation of the exhaustion.

Русский

Исчерпывание компактными множествами можно рассматривать как отображение от натуральных чисел к подмножествам X, где n отображается в K_n — n-ое компактное множество; это обезличивает структуру исчерпания в функцию.

LaTeX

$$$$K\text{ is a function }\mathbb{N} \to 2^{X},\quad K(n)\text{ compact for all }n.$$$$

Lean4

instance : FunLike (CompactExhaustion X) ℕ (Set X)
    where
  coe := toFun
  coe_injective'
    | ⟨_, _, _, _⟩, ⟨_, _, _, _⟩, rfl => rfl

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