mono — Mathlib

English

If m is CountablySeparated and m ≤ m', then m' is CountablySeparated.

Русский

Если m является CountablySeparated и m ≤ m', то m' является CountablySeparated.

LaTeX

$$$ {m m' : MeasurableSpace \\alpha} [hsep : CountablySeparated \\alpha] (h : m ≤ m') : CountablySeparated \\alpha $$$

Lean4

theorem mono {m m' : MeasurableSpace α} [hsep : @CountablySeparated _ m] (h : m ≤ m') : @CountablySeparated _ m' :=
  by
  simp_rw [countablySeparated_def] at *
  rcases hsep with ⟨S, Sct, Smeas, hS⟩
  use S, Sct, (fun s hs ↦ h _ <| Smeas _ hs), hS

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