mem_iff' — Mathlib

English

For all a,b,c in α, a ∈ s(b,c) if and only if a = b or a = c.

Русский

Пусть a,b,c ∈ α. Тогда a принадлежит s(b,c) тогда и только тогда, когда a = b или a = c.

LaTeX

$$$ a \\in s(b,c) \\;\\iff\\; a = b \\lor a = c. $$$

Lean4

@[aesop norm (rule_sets := [Sym2])]
theorem mem_iff' {a b c : α} : Sym2.Mem a s(b, c) ↔ a = b ∨ a = c :=
  { mp := by
      rintro ⟨_, h⟩
      rw [eq_iff] at h
      aesop
    mpr := by
      rintro (rfl | rfl)
      · exact ⟨_, rfl⟩
      rw [eq_swap]
      exact ⟨_, rfl⟩ }

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