le_generateFrom_piiUnionInter — Mathlib

English

If i ∈ S, then generateFrom (π i) ≤ generateFrom (piiUnionInter π S). This is another form of monotonicity in the generating process.

Русский

Если i ∈ S, то generateFrom(π i) ≤ generateFrom(piiUnionInter π S).

LaTeX

$$$\forall x, x \in S \Rightarrow \mathrm{generateFrom}(\pi x) \le \mathrm{generateFrom}(\piiUnionInter(\pi) S)$$$

Lean4

theorem le_generateFrom_piiUnionInter {π : ι → Set (Set α)} (S : Set ι) {x : ι} (hxS : x ∈ S) :
    generateFrom (π x) ≤ generateFrom (piiUnionInter π S) :=
  generateFrom_mono (subset_piiUnionInter hxS)

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