lift'_cong

Mathlib.Order.Filter.Lift

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

← MathLib Explorer

English

If h1 and h2 agree on all s ∈ f, then f.lift' h1 = f.lift' h2.

Русский

Если для каждого s ∈ f верно h1 s = h2 s, то f.lift' h1 = f.lift' h2.

LaTeX

$$$ (hh : ∀ s \\in f, h_1 s = h_2 s) \\Rightarrow f.lift' h_1 = f.lift' h_2 $$$

Lean4

theorem lift'_cong (hh : ∀ s ∈ f, h₁ s = h₂ s) : f.lift' h₁ = f.lift' h₂ :=
  le_antisymm (lift'_mono' fun s hs => le_of_eq <| hh s hs) (lift'_mono' fun s hs => le_of_eq <| (hh s hs).symm)

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

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

Разделы

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

Аффилиация

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