mem_avoid — Mathlib

English

Let α be a generalized Boolean algebra with decidable equality. For any finite partition P of a and any b ∈ α, the blocks of the partition P.avoid b are exactly the sets of the form d \ b, where d runs over the blocks of P and d is not contained in b.

Русский

Пусть α — обобщённая булева алгебра сDecidableEq. Пусть P — конечное разбиение s и для любого b ∈ α множества частей разбиения P.avoid b равны множествам вида d \ b, где d пробегает по частям P и d не подмножество b.

LaTeX

$$$ c \in (P.avoid b).parts \iff \exists d \in P.parts,\ d \nleq b \land d \setminus b = c $$$

Lean4

@[simp]
theorem mem_avoid : c ∈ (P.avoid b).parts ↔ ∃ d ∈ P.parts, ¬d ≤ b ∧ d \ b = c :=
  by
  simp only [avoid, ofErase, mem_erase, Ne, mem_image, ← exists_and_left, @and_left_comm (c ≠ ⊥)]
  refine exists_congr fun d ↦ and_congr_right' <| and_congr_left ?_
  rintro rfl
  rw [sdiff_eq_bot_iff]

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