intersection_covering — Mathlib

English

If R and S are both covering, then their intersection R ⊓ S is also covering.

Русский

Если R и S покрывают, то их пересечение R ⊓ S тоже покрывает.

LaTeX

$$R ∈ J X ∧ S ∈ J X ⇒ R ⊓ S ∈ J X$$

Lean4

/-- The intersection of two covering sieves is covering.

See also [MM92] Chapter III, Section 2, Definition 1 (iv). -/
@[stacks 00Z5 "(1)"]
theorem intersection_covering (rj : R ∈ J X) (sj : S ∈ J X) : R ⊓ S ∈ J X :=
  by
  apply J.transitive rj _ fun Y f Hf => _
  intro Y f hf
  rw [Sieve.pullback_inter, R.pullback_eq_top_of_mem hf]
  simp [sj]

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