inl_mem_sumLift₂ — Mathlib

English

Left case membership: inl c1 belongs to sumLift₂ f g a b iff there exist a1, b1 with a = inl a1, b = inl b1 and c1 ∈ f a1 b1.

Русский

Левый случай членства: inl c1 ∈ sumLift₂ f g a b тогда и только тогда, когда существуют a1, b1 с a = inl a1, b = inl b1 и c1 ∈ f a1 b1.

LaTeX

$$inl c1 ∈ sumLift₂ f g a b ⇔ ∃ a1 b1, a = inl a1 ∧ b = inl b1 ∧ c1 ∈ f a1 b1$$

Lean4

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

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