disjoint_slice_shadow_falling — Mathlib

English

If 𝒜 is an antichain (under inclusion), then the k-th slice 𝒜 #m and the shadow ∂(falling n 𝒜) are disjoint for all m,n.

Русский

Если 𝒜 — антицепь по включению, то 𝒜 #m и тень ∂(falling n 𝒜) дисjoint для любых m,n.

LaTeX

$$$$ (𝒜 \\# m) \\cap \\partial(\\mathrm{falling}_n 𝒜) = \\varnothing $$$$

Lean4

/-- The shadow of `falling m 𝒜` is disjoint from the `n`-sized elements of `𝒜`, thanks to the
antichain property. -/
theorem disjoint_slice_shadow_falling {m n : ℕ} (h𝒜 : IsAntichain (· ⊆ ·) (𝒜 : Set (Finset α))) :
    Disjoint (𝒜 #m) (∂ (falling n 𝒜)) :=
  disjoint_right.2 fun s h₁ h₂ => by
    simp_rw [mem_shadow_iff, mem_falling] at h₁
    obtain ⟨s, ⟨⟨t, ht, hst⟩, _⟩, a, ha, rfl⟩ := h₁
    refine h𝒜 (slice_subset h₂) ht ?_ ((erase_subset _ _).trans hst)
    rintro rfl
    exact notMem_erase _ _ (hst ha)

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