English
The equivalence between compatible families on R and on generate R is constructed by mapping a pair (x, h) to (x.sieveExtend, x.sieveExtend) and back by restricting.
Русский
Эквивалентность между совместимыми семействами на R и на generate R строится через отображение пары (x, h) в (x.sieveExtend, x.sieveExtend) и обратную через ограничение.
LaTeX
$$$\\text{compatibleEquivGenerateSieveCompatible} : { x : FamilyOfElements P R \\;\\text{with } x.Compatible } \\simeq { x : FamilyOfElements P (generate R) \\;\\text{with } x.Compatible }$ with toFun, invFun as in definition$$
Lean4
/-- Given a family of elements `x` for the sieve `S` generated by a presieve `R`, if `x` is restricted
to `R` and then extended back up to `S`, the resulting extension equals `x`.
-/
@[simp]
theorem extend_restrict {x : FamilyOfElements P (generate R).arrows} (t : x.Compatible) :
(x.restrict (le_generate R)).sieveExtend = x :=
by
rw [compatible_iff_sieveCompatible] at t
funext _ _ h
apply (t _ _ _).symm.trans
congr
exact h.choose_spec.choose_spec.choose_spec.2
