biUnion_coe_eq_coe — Mathlib

English

The union, taken over all boxes J whose underlying set coincides with I, of J as sets equals I.

Русский

Объединение по всем коробкам J с условием, что их множество совпадает с I, равно I.

LaTeX

$$$\bigcup_{J : Box ι} (\uparrow J = I) \; (J : Set (ι \to \mathbb{R})) = I$$$

Lean4

theorem biUnion_coe_eq_coe (I : WithBot (Box ι)) : ⋃ (J : Box ι) (_ : ↑J = I), (J : Set (ι → ℝ)) = I := by
  induction I <;> simp

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