mem_of_mem_of_le

Mathlib.Order.PFilter

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

English

If x ∈ F and F ≤ G, then x ∈ G.

Русский

Если x ∈ F и F ≤ G, то x ∈ G.

LaTeX

$$$$ \\forall {F G: PFilter P}, \\; x \\in F \\; \\land \\; F \\le G \\; \\Rightarrow \\; x \\in G. $$$$

Lean4

@[trans]
theorem mem_of_mem_of_le {F G : PFilter P} (hx : x ∈ F) (hle : F ≤ G) : x ∈ G :=
  hle hx

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

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

Разделы

Аффилиация

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