English
Let a ≠ 0. If U is a union of sets of the form Ioi t or Iio t, and V is the preimage of U under x ↦ a·x, then V is again a union of sets of the form Ioi t or Iio t.
Русский
Пусть a ≠ 0.Если U является объединением множест Ioi t и Iio t, и V — предобраз под x ↦ a·x от U, то V снова представляет собой объединение множеств вида Ioi t или Iio t.
LaTeX
$$$\text{If }a\neq 0,\ U=\bigcup_i(Ioi t_i) \cup (Iio s_i) \Rightarrow V=(a··)^{-1}U\in\{s:\,\exists t, s=Ioi t \lor s=Iio t\}$$$
Lean4
theorem preimage_const_mul_Ioi_or_Iio (hb : a ≠ 0) {U V : Set α} (hU : U ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a})
(hV : V = (a * ·) ⁻¹' U) : V ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a} :=
by
obtain ⟨aU, (haU | haU)⟩ := hU <;> simp only [hV, haU, mem_setOf_eq] <;> use a⁻¹ * aU <;>
rcases lt_or_gt_of_ne hb with (hb | hb)
· right; rw [Set.preimage_const_mul_Ioi_of_neg _ hb, div_eq_inv_mul]
· left; rw [Set.preimage_const_mul_Ioi _ hb, div_eq_inv_mul]
· left; rw [Set.preimage_const_mul_Iio_of_neg _ hb, div_eq_inv_mul]
· right; rw [Set.preimage_const_mul_Iio _ hb, div_eq_inv_mul]
