eq_top_pullback — Mathlib

English

Under downward-closedness and pullback properties, the pullback along f of the top sieve equals the top sieve.

Русский

При условии нисходящей замкнутости и свойства вытягивания по f верхний sieve остаётся верхним.

LaTeX

$$$T.pullback f = \top$$$

Lean4

theorem eq_top_pullback {X Y : C} {S T : Sieve X} (h : S ≤ T) (f : Y ⟶ X) (hf : S f) : T.pullback f = ⊤ :=
  by
  ext Z g
  simp only [Sieve.pullback_apply, Sieve.top_apply, iff_true]
  apply h
  apply S.downward_closed
  exact hf

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