English
If s and t are open relations, then their relational composition s ○ t is open.
Русский
Если отношения s и t open (открыты), то их реляционное композиционное произведение s ○ t также открыто.
LaTeX
$$$\\operatorname{IsOpen}(s) \\land \\operatorname{IsOpen}(t) \\Rightarrow \\operatorname{IsOpen}(s \\circ t)$$$
Lean4
theorem relComp [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {s : SetRel α β} {t : SetRel β γ}
(hs : IsOpen s) (ht : IsOpen t) : IsOpen (s ○ t) :=
by
conv => arg 1; equals ⋃ b, (fun p => (p.1, b)) ⁻¹' s ∩ (fun p => (b, p.2)) ⁻¹' t => ext ⟨_, _⟩; simp
exact isOpen_iUnion fun a ↦ hs.preimage (by fun_prop) |>.inter <| ht.preimage (by fun_prop)
