generateFrom_anti — Mathlib

English

If g1 ⊆ g2, then generateFrom(g2) ≤ generateFrom(g1). In words, enlarging the generating family yields a coarser topology.

Русский

Если g1 ⊆ g2, то generateFrom(g2) ≤ generateFrom(g1). Иными словами, увеличение порождающего множества порождает более слабую топологию.

LaTeX

$${\\alpha} {g1 g2 : Set (Set α)} (h : g1 \\subseteq g2) : generateFrom g2 \\le generateFrom g1$$

Lean4

@[mono, gcongr]
theorem generateFrom_anti {α} {g₁ g₂ : Set (Set α)} (h : g₁ ⊆ g₂) : generateFrom g₂ ≤ generateFrom g₁ :=
  (gc_generateFrom _).monotone_u h

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