compl_cIcc — Mathlib

English

The complement of the closed circular interval from a to b equals the open circular interval from b to a.

Русский

Дополнение замкнутого циклического интервала от a до b равно открытому циклическому интервалу от b до a.

LaTeX

$$$(cIcc(a,b))^{c} = cIoo(b,a)$$$

Lean4

theorem compl_cIcc {a b : α} : (cIcc a b)ᶜ = cIoo b a := by
  ext
  rw [Set.mem_cIoo, sbtw_iff_not_btw, cIcc, mem_compl_iff, mem_setOf]

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