English
Let α be a type with a relation r, s a subset of α, and a ∈ α. If for all a,b ∈ α there exists m ∈ α such that for all c ∈ α, r(c,a) ∨ r(c,b) → r(c,m), then Bounded_r(s ∩ {b ∈ α : ¬r(b,a)}) is equivalent to Bounded_r(s).
Русский
Пусть α — множество с отношением r, s — под множество α и a ∈ α. Если для всех a,b существует m ∈ α such that для всех c выполняется r(c,a) ∨ r(c,b) → r(c,m), тогда Bound_r( s ∩ { b | ¬ r(b,a) } ) эквивалентно Bound_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{Bounded}_r\left(s \cap \{b \mid \neg r(b,a)\}\right) \iff \mathrm{Bounded}_r(s)\right).$$$$
Lean4
theorem bounded_inter_not (H : ∀ a b, ∃ m, ∀ c, r c a ∨ r c b → r c m) (a : α) :
Bounded r (s ∩ {b | ¬r b a}) ↔ Bounded r s :=
by
refine ⟨?_, Bounded.mono inter_subset_left⟩
rintro ⟨b, hb⟩
obtain ⟨m, hm⟩ := H a b
exact ⟨m, fun c hc => hm c (or_iff_not_imp_left.2 fun hca => hb c ⟨hc, hca⟩)⟩
