instCanLiftSetCoeIsCompact — Mathlib

English

The inclusion of sets into compact subsets preserves compactness: if a subset is compact, its image as a subset of α is compact.

Русский

Включение множеств в компактные подмножества сохраняет компактность: если подмножество компактно, то оно остаётся компактным как подмножество α.

LaTeX

$$$\text{CanLift }(\mathrm{Set}\,\alpha)(\mathrm{Compacts}\,\alpha)\;\mathrm{instSetLike.coe} \mathrm{IsCompact}$$$

Lean4

instance : CanLift (Set α) (Compacts α) (↑) IsCompact where prf K hK := ⟨⟨K, hK⟩, rfl⟩

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