le_close_of_isClosed — Mathlib

English

If S ≤ T and T is closed, then close S ≤ T.

Русский

Если S ⊆ T и T замкнута, тогда close S ⊆ T.

LaTeX

$$$S \\le T \\Rightarrow J_1.\\mathrm{close} S \\le T$ при $J_1.IsClosed T$$$

Lean4

/-- The closure of a sieve `S` is the largest closed sieve which contains `S` (justifying the name
"closure").
-/
theorem le_close_of_isClosed {X : C} {S T : Sieve X} (h : S ≤ T) (hT : J₁.IsClosed T) : J₁.close S ≤ T := fun _ f hf =>
  hT _ (J₁.superset_covering (Sieve.pullback_monotone f h) hf)

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