mono — Mathlib

English

If μ has finite spanning sets in C and C ⊆ D, then μ has finite spanning sets in D.

Русский

Если μ имеет конечные охватывающие множества в C и C ⊆ D, то μ имеет конечные охватывающие множества в D.

LaTeX

$$$ (h : μ.FiniteSpanningSetsIn C) (hC : C ⊆ D) : μ.FiniteSpanningSetsIn D$$$

Lean4

/-- If `μ` has finite spanning sets in `C` and `C ⊆ D` then `μ` has finite spanning sets in `D`. -/
protected def mono (h : μ.FiniteSpanningSetsIn C) (hC : C ⊆ D) : μ.FiniteSpanningSetsIn D :=
  h.mono' fun _s hs => hC hs.1

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