inter_nonempty — Mathlib

English

Let I and J be ideals in P; if P is directed under ≥, then I ∩ J is nonempty.

Русский

Пусть I и J — идеалы в P; если P направлен относительно отношения ≥, то I ∩ J непусто.

LaTeX

$$(I ∩ J) \neq ∅$$

Lean4

theorem inter_nonempty [IsDirected P (· ≥ ·)] (I J : Ideal P) : (I ∩ J : Set P).Nonempty :=
  by
  obtain ⟨a, ha⟩ := I.nonempty
  obtain ⟨b, hb⟩ := J.nonempty
  obtain ⟨c, hac, hbc⟩ := exists_le_le a b
  exact ⟨c, I.lower hac ha, J.lower hbc hb⟩

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