generateSingleton_eq — Mathlib

English

The sieve generated by the singleton presieve on a morphism f: Y → X equals the sieve generated by a designated singleton operation on f.

Русский

Сито, порождаемое одиночным предсевом по морфизму f: Y → X, равно ситу, порождаемому соответствующей одиночной операцией на f.

LaTeX

$$$$ \mathrm{Sieve.generate}(\mathrm{Presieve.singleton}\ f) = \mathrm{Sieve.generateSingleton} f $$$$

Lean4

theorem generateSingleton_eq {X Y : C} (f : Y ⟶ X) :
    Sieve.generate (Presieve.singleton f) = Sieve.generateSingleton f :=
  by
  ext Z g
  constructor
  · rintro ⟨W, i, p, ⟨⟩, rfl⟩
    exact ⟨i, rfl⟩
  · rintro ⟨g, h⟩
    exact ⟨Y, g, f, ⟨⟩, h⟩

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