English
The inverse of the IicProdIoc equivalence is the pair (frestrictLe₂ hab, restrict₂ Ioc_subset_Iic_self).
Русский
Обратное к эквивалентности IicProdIoc — это пара (frestrictLe₂ hab, restrict₂ Ioc_subset_Iic_self).
LaTeX
$$$(IicProdIoc(a,b))^{\!-1} = (\mathrm{frestrictLe\_2}(a\le b), \mathrm{restrict\_2} Ioc\_subset\_Iic\_self)$$$
Lean4
theorem _root_.IicProdIoc_preimage {a b : ι} (hab : a ≤ b) (s : (i : Iic b) → Set (X i)) :
IicProdIoc a b ⁻¹' (Set.univ.pi s) =
(Set.univ.pi <| frestrictLe₂ (π := (fun n ↦ Set (X n))) hab s) ×ˢ
(Set.univ.pi <| restrict₂ (π := (fun n ↦ Set (X n))) Ioc_subset_Iic_self s) :=
by
ext x
simp only [Set.mem_preimage, Set.mem_pi, Set.mem_univ, IicProdIoc_def, forall_const, Subtype.forall, mem_Iic,
Set.mem_prod, frestrictLe₂_apply, restrict₂, mem_Ioc]
refine ⟨fun h ↦ ⟨fun i hi ↦ ?_, fun i ⟨hi1, hi2⟩ ↦ ?_⟩, fun ⟨h1, h2⟩ i hi ↦ ?_⟩
· convert h i (hi.trans hab)
rw [dif_pos hi]
· convert h i hi2
rw [dif_neg (not_le.2 hi1)]
· split_ifs with hi3
· exact h1 i hi3
· exact h2 i ⟨not_le.1 hi3, hi⟩
