evalFrom_biUnion — Mathlib

English

EvalFrom distributes over a union: evaluating over a union of starting sets equals the union of evaluations over each starting set.

Русский

EvalFrom распределяется по объединению: вычисление по объединению стартовых множеств равно объединению вычислений по каждому стартовому множеству.

LaTeX

$$∀ t f. M.evalFrom(⋃ i ∈ t, f i) x = ⋃ i ∈ t, M.evalFrom(f i) x$$

Lean4

@[simp]
theorem evalFrom_biUnion {ι : Type*} (t : Set ι) (f : ι → Set σ) :
    ∀ (x : List α), M.evalFrom (⋃ i ∈ t, f i) x = ⋃ i ∈ t, M.evalFrom (f i) x
  | [] => by simp
  | a :: x => by simp [stepSet, evalFrom_biUnion _ _ x]

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