English
For a ≤ b ≤ c, the preimage of the universal product-set under IocProdIoc(a,b,c) splits as a product of the left and right preimages, corresponding to the restriction to the right and left blocks.
Русский
Для a ≤ b ≤ c предобраз подуниверсального множества по IocProdIoc(a,b,c) распадается на произведение левой и правой частей, соответствующее ограничению по правому и левому блокам.
LaTeX
$$$\\big(IocProdIoc(a,b,c)\\big)^{-1}(\\mathrm{Set.univ}.pi\, s) = \\big(\\mathrm{Set.univ}.pi\, (\\mathrm{restrict\\_2}\\, (Ioc\\_subset\\_Ioc\\_right\\, hbc) \\, s)\\big) \\times^s \\big(\\mathrm{Set.univ}.pi\, (\\mathrm{restrict\\_2}\\, (Ioc\\_subset\\_Ioc\\_left\\, hab) \\, s)\\big)$$$
Lean4
theorem _root_.IocProdIoc_preimage {a b c : ι} (hab : a ≤ b) (hbc : b ≤ c) (s : (i : Ioc a c) → Set (X i)) :
IocProdIoc a b c ⁻¹' (Set.univ.pi s) =
(Set.univ.pi <| restrict₂ (π := (fun n ↦ Set (X n))) (Ioc_subset_Ioc_right hbc) s) ×ˢ
(Set.univ.pi <| restrict₂ (π := (fun n ↦ Set (X n))) (Ioc_subset_Ioc_left hab) s) :=
by
ext x
simp only [Set.mem_preimage, Set.mem_pi, Set.mem_univ, IocProdIoc, forall_const, Subtype.forall, mem_Ioc,
Set.mem_prod, restrict₂]
refine ⟨fun h ↦ ⟨fun i ⟨hi1, hi2⟩ ↦ ?_, fun i ⟨hi1, hi2⟩ ↦ ?_⟩, fun ⟨h1, h2⟩ i ⟨hi1, hi2⟩ ↦ ?_⟩
· convert h i ⟨hi1, hi2.trans hbc⟩
rw [dif_pos hi2]
· convert h i ⟨lt_of_le_of_lt hab hi1, hi2⟩
rw [dif_neg (not_le.2 hi1)]
· split_ifs with hi3
· exact h1 i ⟨hi1, hi3⟩
· exact h2 i ⟨not_le.1 hi3, hi2⟩
