apply_coe_mem_map

Mathlib.Order.BooleanSubalgebra

URI: https://scilib.ai/kg/mathlib#BooleanSubalgebra.apply_coe_mem_map

English

If a is an element of L (as a member of the subtype), then f(a) ∈ L.map f.

Русский

Если a ∈ L как элемент подтипa, то f(a) ∈ L.map f.

LaTeX

$$$\forall a\in L,\; f(a) \in L.map f$$$

Lean4

theorem apply_coe_mem_map (f : BoundedLatticeHom α β) (a : L) : f a ∈ L.map f :=
  mem_map_of_mem f a.prop

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

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

Разделы

Аффилиация

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