diff_mem

Mathlib.Order.Filter.Basic

URI: https://scilib.ai/kg/mathlib#Filter.diff_mem

English

If s ∈ f and t^c ∈ f, then s \ t ∈ f.

Русский

Если s ∈ f и t^c ∈ f, то s \ t ∈ f.

LaTeX

$$$s \in f \land t^{c} \in f \Rightarrow s \setminus t \in f$$$

Lean4

theorem diff_mem {s t : Set α} (hs : s ∈ f) (ht : tᶜ ∈ f) : s \ t ∈ f :=
  inter_mem hs ht

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

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

Разделы

Аффилиация

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