English
For V, W, M ⊆ β×β with W symmetric, membership in V ○ M ○ W is equivalent to a nonempty ball-based condition.
Русский
Для V, W, M ⊆ β×β и W симметрично, принадлежность в V ○ M ○ W эквивалентна не пустому условию с шарами.
LaTeX
$$$ \forall {V W M : Set (\beta × \beta)} (hW' : IsSymmetricRel W) {p : \beta × \beta},\ p \in V \circ M \circ W \iff (\mathrm{ball} p.1 V \times\, \mathrm{ball} p.2 W \cap M).Nonempty$$$
Lean4
theorem mem_comp_comp {V W M : Set (β × β)} (hW' : IsSymmetricRel W) {p : β × β} :
p ∈ V ○ M ○ W ↔ (ball p.1 V ×ˢ ball p.2 W ∩ M).Nonempty :=
by
obtain ⟨x, y⟩ := p
constructor
· rintro ⟨z, ⟨w, hpw, hwz⟩, hzy⟩
exact ⟨(w, z), ⟨hpw, by rwa [mem_ball_symmetry hW']⟩, hwz⟩
· rintro ⟨⟨w, z⟩, ⟨w_in, z_in⟩, hwz⟩
rw [mem_ball_symmetry hW'] at z_in
exact ⟨z, ⟨w, w_in, hwz⟩, z_in⟩
