compl_cIoo — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem compl_cIoo {a b : α} : (cIoo a b)ᶜ = cIcc b a := by
  ext
  rw [Set.mem_cIcc, btw_iff_not_sbtw, cIoo, mem_compl_iff, mem_setOf]

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