filter

Mathlib.Order.Filter.Pointwise

URI: https://scilib.ai/kg/mathlib#IsUnit.filter

English

If a is a unit in α, then pure a is a unit in Filter α.

Русский

Если a является единицей в α, то чистый фильтр pure a является единицей в Filter α.

LaTeX

$$$\text{IsUnit}(a) \Rightarrow \text{IsUnit}(\text{pure}(a) : \mathrm{Filter}(\alpha)).$$$

Lean4

@[to_additive]
protected theorem _root_.IsUnit.filter : IsUnit a → IsUnit (pure a : Filter α) :=
  IsUnit.map (pureMonoidHom : α →* Filter α)

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

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

Разделы

Аффилиация

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