mem_closed_set_iff — Mathlib

English

If S is generic at x and Z is closed, then x ∈ Z iff S ⊆ Z.

Русский

Если S является обобщением x и Z замкнуто, то x ∈ Z тогда и только тогда S ⊆ Z.

LaTeX

$$$ \mathrm{IsGenericPoint}(x,S) \land \mathrm{IsClosed}(Z) \Rightarrow (x \in Z \iff S \subseteq Z)$$$

Lean4

theorem mem_closed_set_iff (h : IsGenericPoint x S) (hZ : IsClosed Z) : x ∈ Z ↔ S ⊆ Z := by
  rw [← h.def, hZ.closure_subset_iff, singleton_subset_iff]

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