disjoint_of_disjoint_of_mem

Mathlib.Order.Filter.Basic

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

← MathLib Explorer

English

If s ∈ f, t ∈ g and s ⟂ t, then f and g are disjoint.

Русский

Если s ∈ f, t ∈ g и s ⟂ t, то f и g несовместны.

LaTeX

$$Disjoint f g$$

Lean4

theorem disjoint_of_disjoint_of_mem {f g : Filter α} {s t : Set α} (h : Disjoint s t) (hs : s ∈ f) (ht : t ∈ g) :
    Disjoint f g :=
  Filter.disjoint_iff.mpr ⟨s, hs, t, ht, h⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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