notMem_sigmaLift_of_ne_left — Mathlib

English

If the left indices differ, no element of sigmaLift f a b can have that left index; i.e., any element with a1 ≠ x1 is not in sigmaLift f a b.

Русский

Если левые индексы различны, никакой элемент sigmaLift f a b не имеет этого левого индекса; то есть любой элемент с a1 ≠ x1 не принадлежит sigmaLift f a b.

LaTeX

$$$$ x \notin \sigmaLift f a b \quad\text{if } a.1 \neq x.1 $$$$

Lean4

theorem notMem_sigmaLift_of_ne_left (f : ∀ ⦃i⦄, α i → β i → Finset (γ i)) (a : Sigma α) (b : Sigma β) (x : Sigma γ)
    (h : a.1 ≠ x.1) : x ∉ sigmaLift f a b := by
  rw [mem_sigmaLift]
  exact fun H => h H.fst

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