isLocallyConstructible — Mathlib

English

If s is constructible, then it is locally constructible.

Русский

Если множество конструктивно, то оно локально конструктивно.

LaTeX

$$$IsConstructible(s) \\Rightarrow IsLocallyConstructible(s).$$$

Lean4

theorem isLocallyConstructible (hs : IsConstructible s) : IsLocallyConstructible s := fun _ ↦
  ⟨univ, by simp, by simp,
    (isConstructible_preimage_iff_of_isOpenEmbedding isOpen_univ.isOpenEmbedding_subtypeVal (by simp) (by simp)).2 hs⟩

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