coe_comap

Mathlib.Order.Sublattice

URI: https://scilib.ai/kg/mathlib#Sublattice.coe_comap

English

The carrier of L.comap f equals the preimage of L (as a set) under f.

Русский

Носитель L.comap f равен предобразу L по f в виде множества.

LaTeX

$$$(L.comap f) = f^{-1}(L)$$$

Lean4

@[simp, norm_cast]
theorem coe_comap (L : Sublattice β) (f : LatticeHom α β) : L.comap f = f ⁻¹' L :=
  rfl

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

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

Разделы

Аффилиация

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