inter_mem_infs

Mathlib.Data.Finset.Sups

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

English

If s ∈ 𝒜 and t ∈ ℬ, then their intersection lies in 𝒜 ⊼ ℬ: s ∈ 𝒜 ∧ t ∈ ℬ ⇒ s ∩ t ∈ 𝒜 ⊼ ℬ.

Русский

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

LaTeX

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

Lean4

theorem inter_mem_infs : s ∈ 𝒜 → t ∈ ℬ → s ∩ t ∈ 𝒜 ⊼ ℬ :=
  inf_mem_infs

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

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

Разделы

Аффилиация

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