mono' — Mathlib

English

If μ has finite spanning sets in C and C ∩ {s | μ s < ∞} ⊆ D, then μ has finite spanning sets in D.

Русский

Если μ имеет конечные охватывающие множества в C и C ∩ {s | μ(s) < ∞} ⊆ D, то μ имеет конечные охватывающие множества в D.

LaTeX

$$$ (h : μ.FiniteSpanningSetsIn C) (hC : C ∩ {s | μ s < ∞} ⊆ D) : μ.FiniteSpanningSetsIn D$$$

Lean4

/-- If `μ` has finite spanning sets in `C` and `C ∩ {s | μ s < ∞} ⊆ D` then `μ` has finite spanning
sets in `D`. -/
protected def mono' (h : μ.FiniteSpanningSetsIn C) (hC : C ∩ {s | μ s < ∞} ⊆ D) : μ.FiniteSpanningSetsIn D :=
  ⟨h.set, fun i => hC ⟨h.set_mem i, h.finite i⟩, h.finite, h.spanning⟩

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