map_inr_inf_map_inl

Mathlib.Order.Filter.Map

URI: https://scilib.ai/kg/mathlib#Filter.map_inr_inf_map_inl

English

A duplicate formulation of the infimum identity for maps inl and inr.

Русский

Дубликат формулировки тождества наименьшего между map inl и map inr.

LaTeX

$$theorem map_inl_inf_map_inr : map inl f ⊓ map inr g = ⊥$$

Lean4

@[simp]
theorem map_inr_inf_map_inl : map inr f ⊓ map inl g = ⊥ := by rw [inf_comm, map_inl_inf_map_inr]

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

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

Разделы

Аффилиация

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