arrow_max — Mathlib

English

The maximality axiom in arrow form: If S contains the arrow f, then f is covered by S.

Русский

Максимальность в виде стрелки: если f ∈ S, то S покрывает f.

LaTeX

$$S f → J.Covers S f$$

Lean4

/-- The maximality axiom in 'arrow' form: Any arrow `f` in `S` is covered by `S`. -/
theorem arrow_max (f : Y ⟶ X) (S : Sieve X) (hf : S f) : J.Covers S f :=
  by
  rw [Covers, (Sieve.mem_iff_pullback_eq_top f).1 hf]
  apply J.top_mem

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