saturate_of_superset — Mathlib

English

Saturate distributes over supersets: if S ≤ T and S saturates, then T saturates.

Русский

Сатурация распределяется по надмножествам: если S ≤ T и S сатурируется, то T сатурируется.

LaTeX

$$$S \le T \Rightarrow (\text{Saturate } K X S) \Rightarrow (\text{Saturate } K X T)$$$

Lean4

theorem saturate_of_superset (K : Coverage C) {X : C} {S T : Sieve X} (h : S ≤ T) (hS : Saturate K X S) :
    Saturate K X T := by
  apply Saturate.transitive _ _ _ hS
  intro Y g hg
  rw [eq_top_pullback (h := h)]
  · apply Saturate.top
  · assumption

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