denseRange_subtype_val — Mathlib

English

The dense range of Subtype.val is equivalent to density of points satisfying p.

Русский

Плотность образа Subtype.val эквивалентна плотности множества {x | p x}.

LaTeX

$$$@[simp]\\; \\text{denseRange_subtype_val} : DenseRange (\\mathrm{Subtype}.val) \\leftrightarrow Dense (\\{x \\mid p x\\})$$$

Lean4

@[simp]
theorem denseRange_subtype_val {p : X → Prop} : DenseRange (@Subtype.val _ p) ↔ Dense {x | p x} := by simp [DenseRange]

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