English
For any t ⊆ β, the preimage of t under the glued map iUnionLift equals the union, over i, of the image under the inclusion of the preimage of t under f_i.
Русский
Для произвольного t ⊆ β, предобраз отображения, полученного склейкой, равен объединению по i от образов предобразов f_i.
LaTeX
$$$\bigl(iUnionLift S f hf T hT\bigr)^{-1}(t) = \bigcup_{i\in ι} (\text{incl}_i)''(f_i^{-1}(t)).$$$
Lean4
theorem preimage_iUnionLift (t : Set β) :
iUnionLift S f hf T hT ⁻¹' t = inclusion hT ⁻¹' (⋃ i, inclusion (subset_iUnion S i) '' (f i ⁻¹' t)) :=
by
ext x
simp only [mem_preimage, mem_iUnion, mem_image]
constructor
· rcases mem_iUnion.1 (hT x.prop) with ⟨i, hi⟩
refine fun h => ⟨i, ⟨x, hi⟩, ?_, rfl⟩
rwa [iUnionLift_of_mem x hi] at h
· rintro ⟨i, ⟨y, hi⟩, h, hxy⟩
obtain rfl : y = x := congr_arg Subtype.val hxy
rwa [iUnionLift_of_mem x hi]
