English
Let s be a convex absorbent subset of a real vector space E with 0 in s. If gauge(s, x) ≤ 1, then x lies in the closure of s.
Русский
Пусть s — выпукленная абсорбентная подмножество вещественного векторного пространства E, где 0 ∈ s. Если gauge(s, x) ≤ 1, то x принадлежит замыканию s.
LaTeX
$$$ \operatorname{Convex}_{\mathbb{R}}(s) \land 0 \in s \land \operatorname{Absorbent}_{\mathbb{R}}(s) \land \mathrm{gauge}(s,x) \le 1 \Rightarrow x \in \overline{s}$$$
Lean4
theorem mem_closure_of_gauge_le_one (hc : Convex ℝ s) (hs₀ : 0 ∈ s) (ha : Absorbent ℝ s) (h : gauge s x ≤ 1) :
x ∈ closure s :=
by
have : ∀ᶠ r : ℝ in 𝓝[<] 1, r • x ∈ s :=
by
filter_upwards [Ico_mem_nhdsLT one_pos] with r ⟨hr₀, hr₁⟩
apply gauge_lt_one_subset_self hc hs₀ ha
rw [mem_setOf_eq, gauge_smul_of_nonneg hr₀]
exact mul_lt_one_of_nonneg_of_lt_one_left hr₀ hr₁ h
refine mem_closure_of_tendsto ?_ this
exact Filter.Tendsto.mono_left (Continuous.tendsto' (by fun_prop) _ _ (one_smul _ _)) inf_le_left
