coe_compl — Mathlib

English

The underlying set of the complement of s equals the complement of the underlying set: ↑sᶜ = (sᶜ : Set α).

Русский

Основанная множества дополнения над s равна дополнению основания множества: ↑sᶜ = (sᶜ : Set α).

LaTeX

$$$$↑s^{\\complement} = (s^{\\complement} : Set \\alpha).$$$$

Lean4

@[simp]
theorem coe_compl (s : Subtype (MeasurableSet : Set α → Prop)) : ↑sᶜ = (sᶜ : Set α) :=
  rfl

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