# Theory Reachability_Analysis

theory Reachability_Analysis
imports
Flow
Poincare_Map
begin
lemma not_mem_eq_mem_not: "a ∉ A ⟷ a ∈ - A"
by auto
lemma continuous_orderD:
fixes g::"'b::t2_space ⇒ 'c::order_topology"
assumes "continuous (at x within S) g"
shows "g x > c ⟹ ∀⇩_{F} y in at x within S. g y > c"
"g x < c ⟹ ∀⇩_{F} y in at x within S. g y < c"
using order_tendstoD[OF assms[unfolded continuous_within]]
by auto
lemma frontier_halfspace_component_ge: "n ≠ 0 ⟹ frontier {x. c ≤ x ∙ n} = plane n c"
apply (subst (1) inner_commute)
apply (subst (2) inner_commute)
apply (subst frontier_halfspace_ge[of n c])
by auto
lemma closed_Collect_le_within:
fixes f g :: "'a :: topological_space ⇒ 'b::linorder_topology"
assumes f: "continuous_on UNIV f"
and g: "continuous_on UNIV g"
and "closed R"
shows "closed {x ∈ R. f x ≤ g x}"
proof -
have *: "- R ∪ {x. g x < f x} = - {x ∈ R. f x ≤ g x}"
by auto
have "open (-R)" using assms by auto
from open_Un[OF this open_Collect_less [OF g f], unfolded *]
show ?thesis
by (simp add: closed_open)
qed
subsection ‹explicit representation of hyperplanes / halfspaces›