preimage_val_eq_univ_of_subset

Mathlib.Data.Set.Subset

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

English

If A ⊆ B, then the preimage intersection A ↓∩ B equals the universal set (in A).

Русский

Если A ⊆ B, то пересечение A ↓∩ B, рассматриваемое внутри A, равняется все множество.

LaTeX

$$$A \\subseteq B \\implies A \\cap B = A$$$

Lean4

theorem preimage_val_eq_univ_of_subset (h : A ⊆ B) : A ↓∩ B = univ :=
  by
  rw [eq_univ_iff_forall, Subtype.forall]
  exact h

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

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

Разделы

Аффилиация

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