coe_map

Mathlib.Order.UpperLower.CompleteLattice

URI: https://scilib.ai/kg/mathlib#LowerSet.coe_map

English

The coercion of map agrees with the image under the underlying equivalence: coe_map states (map f s : Set β) = f '' s.

Русский

Приведение к коэф-лементу согласуется: (map f s : Set β) = f '' s.

LaTeX

$$$ (\text{map} f\ s : \text{Set}(\beta)) = f '' s $$$

Lean4

@[simp, norm_cast]
theorem coe_map : (map f s : Set β) = f '' s :=
  rfl

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

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

Разделы

Аффилиация

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