image_subset_infs_left

Mathlib.Data.Finset.Sups

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

English

If b ∈ t then s.image (· ⊓ b) ⊆ s ⊼ t.

Русский

Если b ∈ t, то образ s по функции x ↦ x ⊓ b подмножество s ⊼ t.

LaTeX

$$$ b \in t \rightarrow s.image (\cdot \sqcap b) \subseteq s ⊼ t $$$

Lean4

theorem image_subset_infs_left : b ∈ t → s.image (· ⊓ b) ⊆ s ⊼ t :=
  image_subset_image₂_left

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

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

Разделы

Аффилиация

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