Closed IgorPietrzak closed 4 months ago
Level 9 also finished now - found a proof without specialize. Can't split up 𝓟 A = 𝓟 B using le_antisymm in level 10 as we only have a one way implication: ∀ {𝓧 : Type} {𝓕 𝓖 : Filter 𝓧}, 𝓕 ≤ 𝓖 → 𝓖 ≤ 𝓕 → 𝓕 = 𝓖. Not sure how else to go about it.
specialize
le_antisymm
Level 9 also finished now - found a proof without
specialize. Can't split up 𝓟 A = 𝓟 B usingle_antisymmin level 10 as we only have a one way implication: ∀ {𝓧 : Type} {𝓕 𝓖 : Filter 𝓧}, 𝓕 ≤ 𝓖 → 𝓖 ≤ 𝓕 → 𝓕 = 𝓖. Not sure how else to go about it.