isConstructible — Mathlib

English

If f is a functional open embedding, then the image of a constructible set is constructible.

Русский

Если f — открытое вложение функции, то образ конструируемого множества конструируем.

LaTeX

$$$\\forall f:\\ X \\to Y, IsOpenEmbedding(f) \\Rightarrow IsConstructible(s) \\Rightarrow IsConstructible(f''s).$$$

Lean4

theorem _root_.IsCompact.isConstructible (hU' : IsCompact U) (hU : IsOpen U) : IsConstructible U :=
  (hU'.isRetrocompact hU).isConstructible hU

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