ground_subset_closure_iff — Mathlib

English

The closure of the intersection with the ground equals the closure of the whole set when intersected with the ground.

Русский

Замыкание пересечения с основанием равно замыканию полного множества при пересечении с основанием.

LaTeX

$$$M.closure(X \cap M.E) = M.closure X$$$

Lean4

@[simp]
theorem ground_subset_closure_iff : M.E ⊆ M.closure X ↔ M.closure X = M.E := by
  simp [M.closure_subset_ground X, subset_antisymm_iff]

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