inr_mem_sumLift₂ — Mathlib

English

Right case membership: inr c2 belongs to sumLift₂ f g a b iff there exist a2, b2 with a = inr a2, b = inr b2 and c2 ∈ g a2 b2.

Русский

Правый случай членства: inr c2 ∈ sumLift₂ f g a b тогда и только тогда, когда существуют a2, b2 с a = inr a2, b = inr b2 и c2 ∈ g a2 b2.

LaTeX

$$inr c2 ∈ sumLift₂ f g a b ⇔ ∃ a2 b2, a = inr a2 ∧ b = inr b2 ∧ c2 ∈ g a2 b2$$

Lean4

theorem inr_mem_sumLift₂ {c₂ : γ₂} : inr c₂ ∈ sumLift₂ f g a b ↔ ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ c₂ ∈ g a₂ b₂ :=
  by
  rw [mem_sumLift₂, or_iff_right]
  · simp only [inr.injEq, exists_and_left, exists_eq_left']
  rintro ⟨_, _, c₂, _, _, h, _⟩
  exact inr_ne_inl h

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