covering_presieve_eq_self — Mathlib

English

The presieve obtained by pairing coverings and then reassembling via the auxiliary presieve recovers the original presieve.

Русский

Полученный комбинацией покрытий presieve снова возвращает исходный presieve.

LaTeX

$$$(presieveOfCoveringAux (coveringOfPresieve Y R) Y) = R$$$

Lean4

/-- Given a presieve `R` on `Y`, if we take its associated family of opens via `coveringOfPresieve`
(which may not cover `Y` if `R` is not covering), and take the presieve on `Y` associated to the
family of opens via `presieveOfCoveringAux`, then we get back the original presieve `R`. -/
@[simp]
theorem covering_presieve_eq_self {Y : Opens X} (R : Presieve Y) :
    presieveOfCoveringAux (coveringOfPresieve Y R) Y = R :=
  by
  funext Z
  ext f
  exact ⟨fun ⟨⟨_, f', h⟩, rfl⟩ => by rwa [Subsingleton.elim f f'], fun h => ⟨⟨Z, f, h⟩, rfl⟩⟩

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