encard_preimage_val_le_encard_right

Mathlib.Data.Set.Card

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem encard_preimage_val_le_encard_right (P Q : Set α) : (P ↓∩ Q).encard ≤ Q.encard :=
  Function.Embedding.encard_le ⟨fun ⟨⟨x, _⟩, hx⟩ ↦ ⟨x, hx⟩, fun _ _ h ↦ by simpa [Subtype.coe_inj] using h⟩

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

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

Разделы

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

Аффилиация

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