inf_mem

Mathlib.Order.PFilter

URI: https://scilib.ai/kg/mathlib#Order.PFilter.inf_mem

English

If x,y ∈ F and P has a meet, then x ⊓ y ∈ F.

Русский

Если x,y ∈ F и P имеет meet (⊓), то x ⊓ y ∈ F.

LaTeX

$$$$ x \\in F \\land y \\in F \\Rightarrow x \\land y \\in F. $$$$

Lean4

/-- A specific witness of `pfilter.directed` when `P` has meets. -/
theorem inf_mem (hx : x ∈ F) (hy : y ∈ F) : x ⊓ y ∈ F :=
  Ideal.sup_mem hx hy

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

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

Разделы

Аффилиация

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