English
Same as above, expressed with related simplifications for all α, β, f, s, a, and iUnion intersections, clarifying structural equality under Set preimage and iUnion.
Русский
То же самое, но с дополнениями упрощений для общих типов и множеств, показывая структурную эквивалентность через предобраз и iUnion.
LaTeX
$$сложно переписать компактно без контекста; эквивалентная формула приведена в предшествующей записи.$$
Lean4
theorem coe_real_preimage_closedBall_inter_eq {x ε : ℝ} (s : Set ℝ) (hs : s ⊆ closedBall x (|p| / 2)) :
(↑) ⁻¹' closedBall (x : AddCircle p) ε ∩ s = if ε < |p| / 2 then closedBall x ε ∩ s else s :=
by
rcases le_or_gt (|p| / 2) ε with hε | hε
· rcases eq_or_ne p 0 with (rfl | hp)
· simp only [abs_zero, zero_div] at hε
simp only [not_lt.mpr hε, coe_real_preimage_closedBall_period_zero, abs_zero, zero_div, if_false, inter_eq_right]
exact hs.trans (closedBall_subset_closedBall <| by simp [hε])
simp [closedBall_eq_univ_of_half_period_le p hp (↑x) hε, not_lt.mpr hε]
· suffices ∀ z : ℤ, closedBall (x + z • p) ε ∩ s = if z = 0 then closedBall x ε ∩ s else ∅ by
simp [-zsmul_eq_mul, coe_real_preimage_closedBall_eq_iUnion, iUnion_inter, iUnion_ite, this, hε]
intro z
simp only [Real.closedBall_eq_Icc] at hs ⊢
rcases eq_or_ne z 0 with (rfl | hz)
· simp
simp only [hz, zsmul_eq_mul, if_false, eq_empty_iff_forall_notMem]
rintro y ⟨⟨hy₁, hy₂⟩, hy₀⟩
obtain ⟨hy₃, hy₄⟩ := hs hy₀
rcases lt_trichotomy 0 p with (hp | (rfl : 0 = p) | hp)
· rcases Int.cast_le_neg_one_or_one_le_cast_of_ne_zero ℝ hz with hz' | hz'
· have : ↑z * p ≤ -p := by nlinarith
linarith [abs_eq_self.mpr hp.le]
· have : p ≤ ↑z * p := by nlinarith
linarith [abs_eq_self.mpr hp.le]
· simp only [mul_zero, add_zero, abs_zero, zero_div] at hy₁ hy₂ hε
linarith
· rcases Int.cast_le_neg_one_or_one_le_cast_of_ne_zero ℝ hz with hz' | hz'
· have : -p ≤ ↑z * p := by nlinarith
linarith [abs_eq_neg_self.mpr hp.le]
· have : ↑z * p ≤ p := by nlinarith
linarith [abs_eq_neg_self.mpr hp.le]
