English
Let α be a type with a relation r and s a subset. If for all a,b ∈ α there exists m with ∀ c, r(c,a) ∨ r(c,b) → r(c,m), then Unbounded_r(s ∩ {b : ¬ r(b,a)}) holds if and only if Unbounded_r(s) holds.
Русский
Пусть α имеет отношение r, s — подмножество; если для всех a,b существует m с условием ∀ c, r(c,a) ∨ r(c,b) → r(c,m), то Unbounded_r( s ∩ { b | ¬ r(b,a) } ) эквивалентно Unbounded_r(s).
LaTeX
$$$$\left(\forall a,b \in \alpha,\ \exists m \in \alpha,\ \forall c \in \alpha,\ r(c,a) \lor r(c,b) \rightarrow r(c,m)\right) \\Rightarrow \\left(\mathrm{Unbounded}_r\left(s \cap \{b \mid \neg r(b,a)\}\right) \iff \mathrm{Unbounded}_r(s)\right).$$$$
Lean4
theorem unbounded_inter_not (H : ∀ a b, ∃ m, ∀ c, r c a ∨ r c b → r c m) (a : α) :
Unbounded r (s ∩ {b | ¬r b a}) ↔ Unbounded r s := by simp_rw [← not_bounded_iff, bounded_inter_not H]
