superset_covering — Mathlib

English

If S ≤ R and S is covering, then R is covering as well.

Русский

Если S ⊆ R и S покрывает, то и R покрывает.

LaTeX

$$S \leq R \Rightarrow (S ∈ J X) \Rightarrow (R ∈ J X)$$

Lean4

/-- If `S` is a subset of `R`, and `S` is covering, then `R` is covering as well.

See also discussion after [MM92] Chapter III, Section 2, Definition 1. -/
@[stacks 00Z5 "(2)"]
theorem superset_covering (Hss : S ≤ R) (sjx : S ∈ J X) : R ∈ J X :=
  by
  apply J.transitive sjx R fun Y f hf => _
  intro Y f hf
  apply covering_of_eq_top
  rw [← top_le_iff, ← S.pullback_eq_top_of_mem hf]
  apply Sieve.pullback_monotone _ Hss

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