mem_upShadow_iterate_iff_exists_card

English

t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ (t \ s) has cardinality 1.

Русский

t ∈ ∂⁺ 𝒜 эквивалентно существованию s ∈ 𝒜 с s ⊆ t и тем, что #(t \ s) = 1.

LaTeX

$$$ t ∈ ∂⁺ 𝒜 \iff ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = 1 $$$

Lean4

theorem mem_upShadow_iterate_iff_exists_card : t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ u : Finset α, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜 := by
  induction k generalizing t with
  | zero => simp
  | succ k
    ih =>
    simp only [mem_upShadow_iff_erase_mem, ih, Function.iterate_succ_apply', card_eq_succ, subset_erase,
      erase_sdiff_comm, ← sdiff_insert]
    constructor
    · rintro ⟨a, hat, u, rfl, ⟨hut, hau⟩, htu⟩
      exact ⟨_, ⟨_, _, hau, rfl, rfl⟩, insert_subset hat hut, htu⟩
    · rintro ⟨_, ⟨a, u, hau, rfl, rfl⟩, hut, htu⟩
      rw [insert_subset_iff] at hut
      exact ⟨a, hut.1, _, rfl, ⟨hut.2, hau⟩, htu⟩

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