instCompleteLattice — Mathlib

English

If i ∈ I, j ∈ J and x ≤ i ⊔ j, then there exist i' ∈ I, j' ∈ J with x = i' ⊔ j'.

Русский

Если i ∈ I, j ∈ J и x ≤ i ⊔ j, то существуют i' ∈ I, j' ∈ J такие, что x = i' ⊔ j'.

LaTeX

$$$ \forall I,J \in \mathrm{Ideal}(P),\ \forall x,i,j \in P,\ i\in I,\ j\in J,\ x \le i \lor j \Rightarrow \exists i'\in I,\exists j'\in J,\ x = i' \lor j'. $$$

Lean4

instance : CompleteLattice (Ideal P) :=
  { (inferInstance : Lattice (Ideal P)),
    completeLatticeOfInf (Ideal P) fun S ↦
      by
      refine ⟨fun s hs ↦ ?_, fun s hs ↦ by rwa [← coe_subset_coe, coe_sInf, subset_iInter₂_iff]⟩
      rw [← coe_subset_coe, coe_sInf]
      exact biInter_subset_of_mem hs with }

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