dense_iff — Mathlib

English

Dense s in X iff for every x, f x ∈ closure (f '' s).

Русский

Плотноe множество s в X тогда и только тогда, когда для каждого x выполняется f x в замыкании f''s.

LaTeX

$$$\operatorname{Dense}(s) \iff \forall x, f(x) \in \operatorname{closure}(f''(s)).$$$

Lean4

theorem dense_iff (hf : IsInducing f) {s : Set X} : Dense s ↔ ∀ x, f x ∈ closure (f '' s) := by
  simp only [Dense, hf.closure_eq_preimage_closure_image, mem_preimage]

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