piSplitLE_eq

Mathlib.Order.DirectedInverseSystem

URI: https://scilib.ai/kg/mathlib#InverseSystem.piSplitLE_eq

English

The piSplitLE equivalence evaluated at i with a chosen i.e. equals the second component.

Русский

Эквивалентность piSplitLE в точке i с выбранной второй компонентой равна второй компоненте в форме.

LaTeX

$$$\\piSplitLE\\; f\\; ⟨i, \\mathrm{le\_rfl} \\rangle = f.2$$$

Lean4

@[simp]
theorem piSplitLE_eq {f : piLT X i × X i} : piSplitLE f ⟨i, le_rfl⟩ = f.2 := by simp [piSplitLE]

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

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

Разделы

Аффилиация

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