English
For any α, a subset s is measurable in the bottom sigma-algebra if and only if s is empty or s is the whole space.
Русский
Для нижней сигма-алгебры множество измеримо тогда и только тогда, когда оно пусто или равно всему пространству.
LaTeX
$$$\\text{MeasurableSet}[\\perp]\,s \\iff s = \\emptyset \\lor s = \\operatorname{Set.univ}$$$
Lean4
theorem measurableSet_bot_iff {s : Set α} : MeasurableSet[⊥] s ↔ s = ∅ ∨ s = univ :=
let b : MeasurableSpace α :=
{ MeasurableSet' := fun s => s = ∅ ∨ s = univ
measurableSet_empty := Or.inl rfl
measurableSet_compl := by simp +contextual [or_imp]
measurableSet_iUnion := fun _ hf => sUnion_mem_empty_univ (forall_mem_range.2 hf) }
have : b = ⊥ :=
bot_unique fun _ hs =>
hs.elim (fun s => s.symm ▸ @measurableSet_empty _ ⊥) fun s => s.symm ▸ @MeasurableSet.univ _ ⊥
this ▸ Iff.rfl
