compl

Mathlib.Order.Filter.Basic

URI: https://scilib.ai/kg/mathlib#Filter.EventuallyEq.compl

English

If s =^l t, then s^c =^l t^c.

Русский

Если s =^l t, то s^c =^l t^c.

LaTeX

$$$\\\\forall l \\\\ (l : Filter \\\\alpha), \\\\forall s,t \\\\subseteq α, \\\\ (s =^l t) \\\\Rightarrow \\\\ (s^c =^l t^c)$$$

Lean4

@[gcongr]
theorem compl {s t : Set α} {l : Filter α} (h : s =ᶠ[l] t) : (sᶜ : Set α) =ᶠ[l] (tᶜ : Set α) :=
  h.fun_comp Not

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru