English
If u is a neighborhood of 1, there exists V ∈ 𝒩(1) such that for all v,w,s,t ∈ V, v·w·s·t ∈ u.
Русский
Если u — окрестность единицы, существует V ∈ 𝒩(1), такая что для любых v,w,s,t ∈ V сумма произведений v·w·s·t ∈ u.
LaTeX
$$$\forall u\,(u\in 𝒩(1) \Rightarrow \exists V\in 𝒩(1),\forall \{v,w,s,t\}, v\in V \land w\in V \land s\in V \land t\in V \Rightarrow v w s t\in u)$$$
Lean4
@[to_additive exists_nhds_zero_quarter]
theorem exists_nhds_one_split4 {u : Set M} (hu : u ∈ 𝓝 (1 : M)) :
∃ V ∈ 𝓝 (1 : M), ∀ {v w s t}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u :=
by
rcases exists_nhds_one_split hu with ⟨W, W1, h⟩
rcases exists_nhds_one_split W1 with ⟨V, V1, h'⟩
use V, V1
intro v w s t v_in w_in s_in t_in
simpa only [mul_assoc] using h _ (h' v v_in w w_in) _ (h' s s_in t t_in)
