map_le_map

Mathlib.Order.Filter.Map

URI: https://scilib.ai/kg/mathlib#GCongr.Filter.map_le_map

← MathLib Explorer

English

A temporary lemma to tag with gcongr: if F ≤ G then map m F ≤ map m G.

Русский

Временная лемма для маркировки gcongr: если F ≤ G, то map m F ≤ map m G.

LaTeX

$$$[\\text{gcongr}]\\ map\\ m\\ F \\leq map\\ m\\ G$ при $F ≤ G$$$

Lean4

/-- Temporary lemma that we can tag with `gcongr` -/
@[gcongr]
theorem _root_.GCongr.Filter.map_le_map {F G : Filter α} (h : F ≤ G) : map m F ≤ map m G :=
  map_mono h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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