iUnion_smul_eq_setOf_exists — Mathlib

English

The iUnion over g of smul s equals the set of all a with ∃ g, g•a ∈ s.

Русский

Объединение по g эквивалентно множеству всех a, для которых ∃ g: g•a ∈ s.

LaTeX

$$$\bigcup_{g\in\alpha} g\cdot s = \{a \mid \exists g, g\cdot a \in s\}.$$$

Lean4

@[to_additive]
theorem iUnion_smul_eq_setOf_exists {s : Set β} : ⋃ g : α, g • s = {a | ∃ g : α, g • a ∈ s} := by
  simp_rw [← iUnion_setOf, ← iUnion_inv_smul, ← preimage_smul, preimage]

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