lift'_id

Mathlib.Order.Filter.Lift

URI: https://scilib.ai/kg/mathlib#Filter.lift'_id

English

Lifting by the identity map leaves the filter unchanged: f.lift' id = f.

Русский

Подъем по тождественному отображению не изменяет фильтр: f.lift' id = f.

LaTeX

$$$f.lift'\\,\\mathrm{id} = f$$$

Lean4

@[simp]
theorem lift'_id {f : Filter α} : f.lift' id = f :=
  lift_principal2

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

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

Разделы

Аффилиация

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