generateFamily_eq — Mathlib

English

The sieve generated by a presieve of arrows X and π is equal to the sieve generated by the arity family π.

Русский

Сито, порождаемое Presieve.ofArrows X π, равно ситу, порождаемому семейству π.

LaTeX

$$$$ \mathrm{Sieve.generate}(\mathrm{Presieve.ofArrows}\ X\ π) = \mathrm{Sieve.generateFamily} X π $$$$

Lean4

theorem generateFamily_eq {B : C} {α : Type*} (X : α → C) (π : (a : α) → (X a ⟶ B)) :
    Sieve.generate (Presieve.ofArrows X π) = Sieve.generateFamily X π :=
  by
  ext Y g
  constructor
  · rintro ⟨W, g, f, ⟨a⟩, rfl⟩
    exact ⟨a, g, rfl⟩
  · rintro ⟨a, g, rfl⟩
    exact ⟨_, g, π a, ⟨a⟩, rfl⟩

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