mk_mem_sigmaLift — Mathlib

English

For a fixed index i, the element (i,x) belongs to sigmaLift f (i,a) (i,b) exactly when x ∈ f(a,b).

Русский

Для фиксированного индекса i элемент (i,x) принадлежит sigmaLift f( i,a)( i,b ) тогда и только тогда, когда x ∈ f(a,b).

LaTeX

$$$$ (\langle i,x \rangle) \in \sigmaLift f \langle i,a\rangle \langle i,b\rangle \iff x \in f(a,b) $$$$

Lean4

theorem mk_mem_sigmaLift (f : ∀ ⦃i⦄, α i → β i → Finset (γ i)) (i : ι) (a : α i) (b : β i) (x : γ i) :
    (⟨i, x⟩ : Sigma γ) ∈ sigmaLift f ⟨i, a⟩ ⟨i, b⟩ ↔ x ∈ f a b :=
  by
  rw [sigmaLift, dif_pos rfl, mem_map]
  refine ⟨?_, fun hx => ⟨_, hx, rfl⟩⟩
  rintro ⟨x, hx, _, rfl⟩
  exact hx

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