mem_infPrepartition_comm — Mathlib

English

Membership in the infPrepartition is symmetric with respect to swapping the two prepartitions after converting to prepartition form.

Русский

Членство в infPrepartition симметрично относительно обмена двумя предразбиениями после приведения к форме предразбиения.

LaTeX

$$$ J \\in π₁.infPrepartition π₂.toPrepartition \\iff J \\in π₂.infPrepartition π₁.toPrepartition $$$

Lean4

theorem mem_infPrepartition_comm :
    J ∈ π₁.infPrepartition π₂.toPrepartition ↔ J ∈ π₂.infPrepartition π₁.toPrepartition := by
  simp only [← mem_toPrepartition, infPrepartition_toPrepartition, inf_comm]

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