mem_iff_pullback_eq_top — Mathlib

English

For a morphism f: Y → X, S f holds if and only if the pullback of S along f equals the top sieve.

Русский

Для морфизма f: Y → X условие S f истинно тогда и только тогда, когда обратное по f от S равно верхнему ситу.

LaTeX

$$$ S f \\iff S.pullback f = \\top $$$

Lean4

theorem mem_iff_pullback_eq_top (f : Y ⟶ X) : S f ↔ S.pullback f = ⊤ := by
  rw [← id_mem_iff_eq_top, pullback_apply, id_comp]

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