bot_covers — Mathlib

English

For a sieve S on X and a morphism f: Y → X, S covers f in the bottom topology iff f ∈ S.

Русский

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

LaTeX

$$$(\bot_X).Covers(S,f) \ \iff\ \ Sf$$$

Lean4

theorem bot_covers (S : Sieve X) (f : Y ⟶ X) : (⊥ : GrothendieckTopology C).Covers S f ↔ S f := by
  rw [covers_iff, bot_covering, ← Sieve.mem_iff_pullback_eq_top]

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