English
Dense range of integer powers holds iff the map is surjective; symmetric statement for the additive version.
Русский
Плотность диапазона целочисленных степеней эквивалентна сюръективности; аналогично для аддитивной версии.
LaTeX
$$$\text{DenseRange}(a^{\cdot}: \mathbb{Z} \to G) \iff \text{Surjective}(a^{\cdot}: \mathbb{Z} \to G).$$$
Lean4
/-- `limsup (c - xᵢ) = c - liminf xᵢ`. -/
theorem limsup_const_sub (F : Filter ι) [AddCommSemigroup R] [Sub R] [ContinuousSub R] [OrderedSub R] [AddLeftMono R]
(f : ι → R) (c : R) (cobdd : F.IsCoboundedUnder (· ≥ ·) f) (bdd_below : F.IsBoundedUnder (· ≥ ·) f) :
Filter.limsup (fun i ↦ c - f i) F = c - Filter.liminf f F :=
by
rcases F.eq_or_neBot with rfl | _
· simp only [liminf, limsInf, limsup, limsSup, map_bot, eventually_bot, Set.setOf_true]
simp only [IsCoboundedUnder, IsCobounded, map_bot, eventually_bot, true_implies] at cobdd
rcases cobdd with ⟨x, hx⟩
refine (csInf_le ?_ (Set.mem_univ _)).antisymm (tsub_le_iff_tsub_le.1 (le_csSup ?_ (Set.mem_univ _)))
· refine ⟨x - x, mem_lowerBounds.2 fun y ↦ ?_⟩
simp only [Set.mem_univ, true_implies]
exact tsub_le_iff_tsub_le.1 (hx (x - y))
· refine ⟨x, mem_upperBounds.2 fun y ↦ ?_⟩
simp only [Set.mem_univ, hx y, implies_true]
·
exact
(Antitone.map_limsInf_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ c - x)
(fun _ _ h ↦ tsub_le_tsub_left h c) (continuous_sub_left c).continuousAt cobdd bdd_below).symm
