and

Mathlib.Topology.Sheaves.LocalPredicate

URI: https://scilib.ai/kg/mathlib#TopCat.PrelocalPredicate.and

Lean4

/-- The conjunction of two prelocal predicates is prelocal. -/
def and (P Q : PrelocalPredicate T) : PrelocalPredicate T
    where
  pred f := P.pred f ∧ Q.pred f
  res i f h := ⟨P.res i f h.1, Q.res i f h.2⟩

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

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

Разделы

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

Аффилиация

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