mem_sumLexLift — Mathlib

English

Characterization of membership in sumLexLift: c ∈ sumLexLift f1 f2 g1 g2 a b iff one of four corresponding existence conditions holds.

Русский

Характеризация членства в sumLexLift: c ∈ sumLexLift f1 f2 g1 g2 a b эквивалентно одному из четырех соответствующих условий существования.

LaTeX

$$c ∈ sumLexLift f1 f2 g1 g2 a b ⇔ (∃ a1 b1 c1, a = inl a1 ∧ b = inl b1 ∧ c = inl c1 ∧ c1 ∈ f1 a1 b1) ∨ (∃ a1 b2 c1, a = inl a1 ∧ b = inr b2 ∧ c = inl c1 ∧ c1 ∈ g1 a1 b2) ∨ (∃ a1 b2 c2, a = inl a1 ∧ b = inr b2 ∧ c = inr c2 ∧ c2 ∈ g2 a1 b2) ∨ (∃ a2 b2 c2, a = inr a2 ∧ b = inr b2 ∧ c = inr c2 ∧ c2 ∈ f2 a2 b2)$$

Lean4

theorem mem_sumLexLift :
    c ∈ sumLexLift f₁ f₂ g₁ g₂ a b ↔
      (∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
        (∃ a₁ b₂ c₁, a = inl a₁ ∧ b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
          (∃ a₁ b₂ c₂, a = inl a₁ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
            ∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂ :=
  by
  constructor
  · obtain a | a := a <;> obtain b | b := b
    · rw [sumLexLift, mem_map]
      rintro ⟨c, hc, rfl⟩
      exact Or.inl ⟨a, b, c, rfl, rfl, rfl, hc⟩
    · refine fun h ↦ (mem_disjSum.1 h).elim ?_ ?_
      · rintro ⟨c, hc, rfl⟩
        exact Or.inr (Or.inl ⟨a, b, c, rfl, rfl, rfl, hc⟩)
      · rintro ⟨c, hc, rfl⟩
        exact Or.inr (Or.inr <| Or.inl ⟨a, b, c, rfl, rfl, rfl, hc⟩)
    · exact fun h ↦ (notMem_empty _ h).elim
    · rw [sumLexLift, mem_map]
      rintro ⟨c, hc, rfl⟩
      exact Or.inr (Or.inr <| Or.inr <| ⟨a, b, c, rfl, rfl, rfl, hc⟩)
  · rintro
      (⟨a, b, c, rfl, rfl, rfl, hc⟩ | ⟨a, b, c, rfl, rfl, rfl, hc⟩ | ⟨a, b, c, rfl, rfl, rfl, hc⟩ |
          ⟨a, b, c, rfl, rfl, rfl, hc⟩)
    · exact mem_map_of_mem _ hc
    · exact inl_mem_disjSum.2 hc
    · exact inr_mem_disjSum.2 hc
    · exact mem_map_of_mem _ hc

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