mem_or_mem — Mathlib

English

For a Boolean lattice, IsPrime I implies: if x ⊓ y ∈ I, then x ∈ I or y ∈ I.

Русский

В булевой решётке: если x ⊓ y ∈ I, то x ∈ I или y ∈ I.

LaTeX

$$$\\forall x,y:\\; x \\land y \\in I \\Rightarrow x \\in I \\lor y \\in I$$$

Lean4

theorem mem_or_mem (hI : IsPrime I) {x y : P} : x ⊓ y ∈ I → x ∈ I ∨ y ∈ I :=
  by
  contrapose!
  let F := hI.compl_filter.toPFilter
  change x ∈ F ∧ y ∈ F → x ⊓ y ∈ F
  exact fun h => inf_mem h.1 h.2

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