mem_biUnionTagged — Mathlib

English

A box J belongs to the biUnionTagged of π with πi if and only if there is some J' in π such that J belongs to πi(J').

Русский

Коробка J принадлежит biUnionTagged(πi) тогда и только тогда, когда существует J' в π, такая что J принадлежит πi(J').

LaTeX

$$$ J \\in \\pi.biUnionTagged \\pi_i \\iff \\exists J' \\in \\pi,\\; J \\in \\pi_i(J') $$$

Lean4

@[simp]
theorem mem_biUnionTagged (π : Prepartition I) {πi : ∀ J, TaggedPrepartition J} :
    J ∈ π.biUnionTagged πi ↔ ∃ J' ∈ π, J ∈ πi J' :=
  π.mem_biUnion

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