ofLE — Mathlib

English

Given ν ≤ μ and a μ-FiniteSpanningSetsIn S, we obtain a ν-FiniteSpanningSetsIn S.

Русский

При условии ν ≤ μ и существовании μ-FiniteSpanningSetsIn S получаем ν-FiniteSpanningSetsIn S.

LaTeX

$$def ofLE (h : ν ≤ μ) {C : Set (Set α)} (S : μ.FiniteSpanningSetsIn C) : ν.FiniteSpanningSetsIn C$$

Lean4

/-- Given measures `μ`, `ν` where `ν ≤ μ`, `FiniteSpanningSetsIn.ofLe` provides the induced
`FiniteSpanningSet` with respect to `ν` from a `FiniteSpanningSet` with respect to `μ`. -/
def ofLE (h : ν ≤ μ) {C : Set (Set α)} (S : μ.FiniteSpanningSetsIn C) : ν.FiniteSpanningSetsIn C
    where
  set := S.set
  set_mem := S.set_mem
  finite n := lt_of_le_of_lt (le_iff'.1 h _) (S.finite n)
  spanning := S.spanning

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