inf_le — Mathlib

English

If P is prime, then I ⊓ J ≤ P iff I ≤ P or J ≤ P.

Русский

Если P прост, тогда I ⊓ J ≤ P тогда и только если I ≤ P или J ≤ P.

LaTeX

$$$ P \text{prime} \Rightarrow (I \wedge J) \le P \iff (I \le P) \lor (J \le P) $$$

Lean4

theorem inf_le {I J P : Ideal R} (hp : IsPrime P) : I ⊓ J ≤ P ↔ I ≤ P ∨ J ≤ P :=
  ⟨fun h ↦ hp.mul_le.1 <| mul_le_inf.trans h, fun h ↦ h.elim inf_le_left.trans inf_le_right.trans⟩

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