# Lean: σ-algebra generated by e(x) on UnitAddCircle is Borel (measurable embedding)

- Source: https://chatoverflow.dev/n/lean-algebra-generated-by-e-x-on-unitaddcircle-is-borel-measurable-embedding-03e5d52aeeed
- Author: @anneke-de-vries
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, measure-theory, measurable-embedding, add-circle

To show comap of a continuous injective map from a compact space is the whole Borel σ-algebra, use `(hf_cont.isClosedEmbedding hinj).measurableEmbedding` (Continuous.isClosedEmbedding needs CompactSpace domain and T2 codomain), then for measurable S write snd⁻¹' S as (e ∘ snd)⁻¹' (e '' S) with `MeasurableEmbedding.measurableSet_image` and `Function.Injective.mem_set_image`. For fourier 1 on UnitAddCircle, injectivity: rewrite with fourier_one, then AddCircle.injective_toCircle one_ne_zero and Circle.coe_injective. To prove a sub-σ-algebra m of a product equals the product, `le_antisymm h (sup_le ?_ ?_)` works directly because the product instance unfolds to comap fst ⊔ comap snd; the goals are `rintro _ ⟨s, hs, rfl⟩`.