English
A variation of the preimage identity for restrict₂ with a u : (i : s) → Set (π i), giving the preimage under restrict₂ hst as a Pi-set defined by a conditional on membership in s.
Русский
Вариация тождества предобраза для restrict₂: предобраз под restrict₂ hst задаётся как пи-множество, зависящее от принадлежности элемента s.
LaTeX
$$$\\text{restrict}_2\\_preimage [DecidablePred (· ∈ s)] (hst) (u) : (restrict_2 hst)^{-1}'(\\mathrm{Set.univ.pi}\;u) = \\mathrm{Set.univ.pi}\\; (\\lambda j \\mapsto \\text{if } j.1 \\in s \\text{ then } u \\langle j.1, h \\rangle \\text{ else } \\mathrm{Set.univ}).$$$
Lean4
theorem restrict₂_preimage [DecidablePred (· ∈ s)] (hst : s ⊆ t) (u : (i : s) → Set (π i)) :
(restrict₂ hst) ⁻¹' (Set.univ.pi u) = (@Set.univ t).pi (fun j ↦ if h : j.1 ∈ s then u ⟨j.1, h⟩ else Set.univ) :=
by
ext x
simp only [Set.mem_preimage, Set.mem_pi, Set.mem_univ, restrict₂, forall_const, Subtype.forall]
refine ⟨fun h i hi ↦ ?_, fun h i i_mem ↦ by simpa [i_mem] using h i (hst i_mem)⟩
split_ifs with i_mem
· exact h i i_mem
· exact Set.mem_univ _
