mem_inf — Mathlib

English

For prepartitions π1 and π2, J belongs to the infimum π1 ⊓ π2 if and only if there exist J1 ∈ π1 and J2 ∈ π2 with J equal to J1 ⊓ J2 in the box-with-bot sense.

Русский

Для предразбиений π1 и π2 элемент J принадлежит их наименьшему элементу π1 ⊓ π2 тогда, когда найдутся J1 ∈ π1 и J2 ∈ π2 такие, что J = J1 ⊓ J2 в конструкции BoxWithBot.

LaTeX

$$$ J \in π_1 \sqcap π_2 \;\iff\; \exists J_1 \in π_1, \exists J_2 \in π_2, (J : WithBot(Box \ ι)) = \uparrow J_1 \sqcap \uparrow J_2. $$$

Lean4

@[simp]
theorem mem_inf {π₁ π₂ : Prepartition I} : J ∈ π₁ ⊓ π₂ ↔ ∃ J₁ ∈ π₁, ∃ J₂ ∈ π₂, (J : WithBot (Box ι)) = ↑J₁ ⊓ ↑J₂ := by
  simp only [inf_def, mem_biUnion, mem_restrict]

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