I found this definition in Isabelle definition (in topological_space) nhds :: "’a ⇒ ‘a filter" where "nhds a = (INF S∈{S. open S ∧ a ∈ S}. principal S)" What is INF? I can’t find anything in query tab nor can I jump to definition with Ctrl+Click. >Solution : In Isabelle, INF is a constant… Read More What is INF in Isabelle