dense_iff — Mathlib

English

A further simplified form of mem_closure_range_iff using basic natural-number bounds.

Русский

Ещё более простая форма mem_closure_range_iff_nat с использованием элементарных ограничений по натуральным числам.

LaTeX

$$$\text{(simplified form)}$$$

Lean4

theorem dense_iff {s : Set α} : Dense s ↔ ∀ x, ∀ r > 0, (ball x r ∩ s).Nonempty :=
  forall_congr' fun x => by simp only [mem_closure_iff, Set.Nonempty, mem_inter_iff, mem_ball', and_comm]

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