card_infs_le

Mathlib.Data.Finset.Sups

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

English

The number of pairwise infima is at most the product of the cardinalities: |s ⊼ t| ≤ |s| · |t|.

Русский

Число попарных инфимумов не превосходит произведение кардиналий: |s ⊼ t| ≤ |s| · |t|.

LaTeX

$$$ |s ⊼ t| \le |s| \cdot |t| $$$

Lean4

theorem card_infs_le : #(s ⊼ t) ≤ #s * #t :=
  card_image₂_le _ _ _

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

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

Разделы

Аффилиация

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