Theorem: 𝓑_const (RMT4/Spaces.lean)

State before:
U : Set ℂ
Q✝ : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
Q : Set ℂ
⊢ (𝓑 U fun x => Q) = {f | f ∈ 𝓗 U ∧ MapsTo f U Q}
Tactic:
simp [𝓑, ← mapsTo_sUnion]
State after:
no goals