close_isClosed — Mathlib

English

The closure of a sieve is closed: for every g, the arrow is closed under closure.

Русский

Замыкание ситы является закрытым: для любого стрелка переход замыкания сохраняется.

LaTeX

$$$J_1.\\mathrm{IsClosed}(J_1.\\mathrm{close} S)$$$

Lean4

/-- The closure of a sieve is closed. -/
theorem close_isClosed {X : C} (S : Sieve X) : J₁.IsClosed (J₁.close S) := fun _ g hg =>
  J₁.arrow_trans g _ S hg fun _ hS => hS

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