intrinsicClosure_nonempty — Mathlib

English

For any admissible structures, the intrinsic closure of a subset s of P is nonempty if and only if s is nonempty.

Русский

Для допустимых структур внутренняя замкнутость множества s ⊆ P непусто тогда и только тогда, когда s непусто.

LaTeX

$$$(\\operatorname{intrinsicClosure}_{\\mathbb{k}}(s)) \\neq \\varnothing \\iff s \\neq \\varnothing$$$

Lean4

@[simp]
theorem intrinsicClosure_nonempty : (intrinsicClosure 𝕜 s).Nonempty ↔ s.Nonempty :=
  ⟨by simp_rw [nonempty_iff_ne_empty]; rintro h rfl; exact h intrinsicClosure_empty,
    Nonempty.mono subset_intrinsicClosure⟩

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