mem_image_const_self

Mathlib.Data.Finset.Image

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

English

Special case: b in image of constant b equals nonempty set iff s is nonempty.

Русский

Особый случай: элемент b принадлежит образу константы b тогда и только тогда, когда s непусто.

LaTeX

$$$b \\in \\operatorname{image}(\\lambda x. b, s) \\iff s.Nonempty$$

Lean4

theorem mem_image_const_self : b ∈ s.image (const α b) ↔ s.Nonempty :=
  mem_image_const.trans <| and_iff_left rfl

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

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

Разделы

Аффилиация

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