encard_preimage_val_le_encard_left

Mathlib.Data.Set.Card

URI: https://scilib.ai/kg/mathlib#Set.encard_preimage_val_le_encard_left

English

The encard of P ∩ Q is bounded by the encard of P: (P ∩ Q).encard ≤ P.encard.

Русский

encard пересечения ≤ encard первого множества.

LaTeX

$$$ (P \\cap Q).encard \\le P.encard $$$

Lean4

theorem encard_preimage_val_le_encard_left (P Q : Set α) : (P ↓∩ Q).encard ≤ P.encard :=
  (Function.Embedding.subtype _).encard_le

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

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

Разделы

Аффилиация

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