exists_distinct_prev_or — Mathlib

English

For a no-loop complex shape, either there exists a distinct previous relation or every previous relation fails.

Русский

Для формы без петли либо существует отличное предыдущее отношение, либо для каждого предыдущего отношения оно неверно.

LaTeX

$$$\exists k: c.Rel(j,k) \wedge j \neq k \; \lor \; \forall k, \neg c.Rel(j,k)$$$

Lean4

theorem exists_distinct_prev_or : (∃ (k : ι), c.Rel j k ∧ j ≠ k) ∨ ∀ (k : ι), ¬c.Rel j k :=
  by
  by_cases h : ∃ (k : ι), c.Rel j k
  · obtain ⟨k, hk⟩ := h
    exact Or.inl ⟨k, hk, fun hjk ↦ c.not_rel_of_eq hjk hk⟩
  · exact Or.inr (by simpa using h)

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