disjSups_subset_iff

Mathlib.Data.Finset.Sups

URI: https://scilib.ai/kg/mathlib#Finset.disjSups_subset_iff

English

If s ∈ 𝒜 and t ∈ ℬ, then their intersection belongs to 𝒜 ⊼ ℬ.

Русский

Если s принадлежит 𝒜, а t принадлежит ℬ, то их пересечение принадлежит 𝒜 ⊼ ℬ.

LaTeX

$$$ s \in 𝒜 \to t \in ℬ \to s \cap t \in 𝒜 \nabla ℬ $$$

Lean4

@[simp]
theorem disjSups_subset_iff : s ○ t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → a ⊔ b ∈ u :=
  forall_disjSups_iff

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

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

Разделы

Аффилиация

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