preimage_liftCover — Mathlib

English

For t ⊆ β, the preimage of t under liftCover equals the union over i of the image of f_i⁻¹(t) under the inclusion of S_i into α.

Русский

Для t ⊆ β предобраз liftCover равен объединению по i от образа f_i⁻¹(t) через включения S_i → α.

LaTeX

$$$(\text{liftCover}(S,f,hf,hS))^{-1}(t) = \bigcup_{i\in ι} (\text{incl}_i)''(f_i^{-1}(t)).$$$

Lean4

theorem preimage_liftCover (t : Set β) : liftCover S f hf hS ⁻¹' t = ⋃ i, (↑) '' (f i ⁻¹' t) :=
  by
  change (iUnionLift S f hf univ hS.symm.subset ∘ fun a => ⟨a, mem_univ a⟩) ⁻¹' t = _
  rw [preimage_comp, preimage_iUnionLift]
  ext; simp

Похожие утверждения